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


Conclusion

1. add(choose(vert(G!1)), union(r1(G!1), r2(G!1))) = vert(G!1)
2. (card(r1(G!1)) + card(r2(G!1))) > = (size(G!1) - 1)


Tactic
HIDE 2

Premise 1.   (has proof of 2 steps)

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