FDL > PVS > Graphs > ramsey new > r2 TCC1 > pf:r2 TCC1 > 1 > 2 > 1 > 1 > 1 > 1

Conclusion

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

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