FDL > PVS > Graphs > subgraphs > subgraph TCC2 > pf:subgraph TCC2 > 1 (6 nodes)

Conclusion

1. is finite[T]({i:T | vert(G!1)(i) AND V!1(i)})

Tactic
 LEMMA "finite_subset[T]"
Premise 1.   (has proof of 5 steps)

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

1. is finite[T]({i:T | vert(G!1)(i) AND V!1(i)})