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

Conclusion

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

Tactic
 PROP
Premise 1.   (has proof of 1 step)

1. subset?({i:T | vert(G!1)(i) AND V!1(i)}, vert(G!1))
Premise 2.   (has proof of 1 step)

1. subset?({e:doubleton[T] | edges(G!1)(e) AND (FORALL x:T : e(x) IMPLIES V!1(x))}, edges(G!1))