let G2 be Subgraph of G; :: thesis: G2 is vertex-finite
the_Vertices_of G2 c= the_Vertices_of G ;
hence G2 is vertex-finite ; :: thesis: verum