FDL > PVS > Graphs > ramsey new > card r1 r2 > pf:card r1 r2 > 1 > 2 > 1 > 1

Conclusion

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