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

Conclusion

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

Tactic
 TYPEPRED "G!1"
Premise 1.   (has proof of 1 step)

-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))