let G2 be Subgraph of G; :: thesis: G2 is finite
( the_Vertices_of G2 is finite & the_Edges_of G2 is finite ) ;
hence G2 is finite by Def19; :: thesis: verum