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

Conclusion

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