FDL > PVS > Graphs > ramsey new > r1 TCC2 > pf:r1 TCC2 > 1 > 2 > 1 > 1 > 1 (2 nodes)

Conclusion

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

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

Tactic
 EXPAND "member"
Premise 1.   (has proof of 1 step)

-1. vert(G!1)(x!1) AND (x!1 /= choose[T](vert(G!1))) AND edge?[T](G!1)(choose[T](vert(G!1)), x!1)

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