FDL > PVS > Graphs > subgraphs > subgraph TCC1 > pf:subgraph TCC1 > 1 > 1 (5 nodes)

Conclusion

-1. FORALL A:finite set[doubleton[T]], S:set[doubleton[T]] : subset?(S, A) IMPLIES is finite(S)

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

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

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

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