FDL > PVS > Graphs > subgraphs > subgraph vert sub > pf:subgraph vert sub > 1 > 1 > 1 > 1 (4 nodes)

Conclusion

-1. FORALL x:T : member(x, V!1) = > member(x, vert(G!1))

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

Tactic
 INST?
Premise 1.   (has proof of 3 steps)

-1. member(x!1, V!1) = > member(x!1, vert(G!1))

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