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

Conclusion

-1. FORALL e:doubleton[T] : edges(G!1)(e) IMPLIES (FORALL x:T : e(x) IMPLIES vert(G!1)(x))
-2. nonempty?[T](vert(G!1))

1. nonempty?[T](vert(G!1))