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

Conclusion

1. (card(r1(G!1)) + card(r2(G!1))) > = ((card(union(r1(G!1), r2(G!1))) + IF union(r1(G!1), r2(G!1))(choose(vert(G!1))) THEN 0 ELSE 1 ENDIF) - 1)

Tactic
 REWRITE "card_union"
Premise 1.   (has proof of 2 steps)

1. (card(r1(G!1)) + card(r2(G!1))) > = ((((card(r1(G!1)) + card(r2(G!1))) - card(intersection(r1(G!1), r2(G!1)))) + IF union(r1(G!1), r2(G!1))(choose(vert(G!1))) THEN 0 ELSE 1 ENDIF) - 1)