FDL > PVS > Graphs > ramsey new > r2 TCC1 > pf:r2_TCC1 : proof (10 nodes)

Conclusion

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

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

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 (NOT edge?[T](G!1)(v0, n))})