FDL > PVS > Graphs > subgraphs > subgraph TCC3 > pf:subgraph TCC3 > 1 > 1 > 1 > 1 > 1 (6 nodes)

Conclusion

-1. FORALL e:doubleton[T] : edges(G!1)(e) IMPLIES (FORALL x:T : e(x) IMPLIES vert(G!1)(x))
-2. edges(G!1)(e!1) AND (FORALL x:T : e!1(x) IMPLIES V!1(x))
-3. e!1(x!1)

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