FDL > PVS > Graphs > ramsey new > card r1 r2 > pf:card r1 r2 > 1 > 1 > 1 (6 nodes)

Conclusion

-1. add(choose(vert(G!1)), union(r1(G!1), r2(G!1))) = vert(G!1)

1. (card(r1(G!1)) + card(r2(G!1))) > = (card[T](vert(G!1)) - 1)

Tactic
 REPLACE "-1" * RL
Premise 1.   (has proof of 5 steps)

-1. add(choose(vert(G!1)), union(r1(G!1), r2(G!1))) = vert(G!1)

1. (card(r1(G!1)) + card(r2(G!1))) > = (card[T](add(choose(vert(G!1)), union(r1(G!1), r2(G!1)))) - 1)