let G2 be inducedSubgraph of G,V,E; :: thesis: not G2 is vertex-finite
per cases ( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) or not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ;
suppose ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) ; :: thesis: not G2 is vertex-finite
hence not G2 is vertex-finite by GLIB_000:def 37; :: thesis: verum
end;
suppose ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ; :: thesis: not G2 is vertex-finite
then G == G2 by GLIB_000:def 37;
hence not G2 is vertex-finite by Th8; :: thesis: verum
end;
end;