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

Conclusion

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

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

Tactic
 INST "-1" "vert(G!1)"
Premise 1.   (has proof of 3 steps)

-1. subset?({i:T | vert(G!1)(i) AND V!1(i)}, vert(G!1)) IMPLIES is finite({i:T | vert(G!1)(i) AND V!1(i)})

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