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

Conclusion

-1. FORALL x:T : e!1(x) IMPLIES vert(G!1)(x)
-2. edges(G!1)(e!1)
-3. V!1(x!1)
-4. e!1(x!1)

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

Tactic
 INST?
Premise 1.   (has proof of 1 step)

-1. e!1(x!1) IMPLIES vert(G!1)(x!1)
-2. edges(G!1)(e!1)
-3. V!1(x!1)
-4. e!1(x!1)

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