FDL > PVS > Graphs > ramsey new > r1 TCC2 > pf:r1 TCC2 > 1 > 1 > 1 > 1

Conclusion

-1. subset?({n:T | vert(G!1)(n) AND (n /= choose[T](vert(G!1))) AND edge?[T](G!1)(choose[T](vert(G!1)), n)}, vert(G!1)) IMPLIES is finite({n:T | vert(G!1)(n) AND (n /= choose[T](vert(G!1))) AND edge?[T](G!1)(choose[T](vert(G!1)), n)})
-2. subset?({n:T | vert(G!1)(n) AND (n /= choose[T](vert(G!1))) AND edge?[T](G!1)(choose[T](vert(G!1)), n)}, vert(G!1))

1. is finite[T](LET (v0:(vert(G!1)) ) = choose[T](vert(G!1)) IN
{n:T | vert(G!1)(n) AND (n /= v0) AND edge?[T](G!1)(v0, n)})