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 ; :: thesis: verum