let IT be inducedSubgraph of G,V,E; :: thesis: IT is finite
( the_Vertices_of IT = V & the_Edges_of IT = E ) by Def39;
hence IT is finite by Def19; :: thesis: verum