FDL > PVS > Graphs > subgraphs > finite vert subset > pf:finite vert subset > 1 > 1 > 1 > 1 (3 nodes)

Conclusion

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

1. is finite(LAMBDA i:T : vert(G!1)(i) AND V!1(i))

Tactic
 ASSERT
Premise 1.   (has proof of 2 steps)

1. subset?(LAMBDA i:T : vert(G!1)(i) AND V!1(i), vert(G!1))
2. is finite(LAMBDA i:T : vert(G!1)(i) AND V!1(i))