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


Conclusion

-1. edges(G!1 WITH [vert := {i:T | vert(G!1)(i) AND V!1(i)}, edges := {e:doubleton[T] | edges(G!1)(e) AND (FORALL x:T : e(x) IMPLIES V!1(x))}])(e!1)
-2. e!1(x!1)

1. vert(G!1 WITH [vert := {i:T | vert(G!1)(i) AND V!1(i)}, edges := {e:doubleton[T] | edges(G!1)(e) AND (FORALL x:T : e(x) IMPLIES V!1(x))}])(x!1)


Tactic
ASSERT

Premise 1.   (has proof of 7 steps)

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

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