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

Conclusion

1. FORALL x:T : member(x, {n:T | vert(G!1)(n) AND (n /= choose[T](vert(G!1))) AND (NOT edge?[T](G!1)(choose[T](vert(G!1)), n))}) = > member(x, vert(G!1))

Tactic
 SKOSIMP*
Premise 1.   (has proof of 2 steps)

-1. member(x!1, {n:T | vert(G!1)(n) AND (n /= choose[T](vert(G!1))) AND (NOT edge?[T](G!1)(choose[T](vert(G!1)), n))})

1. member(x!1, vert(G!1))