FDL > PVS > Graphs > subgraphs > subgraph TCC1 > pf:subgraph_TCC1 : proof (7 nodes)

Conclusion

1. FORALL G:graph[T], V:set[T] : is finite[doubleton[T]]({e:doubleton[T] | edges(G)(e) AND (FORALL x:T : e(x) IMPLIES V(x))})

Tactic
 SKOSIMP*
Premise 1.   (has proof of 6 steps)

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