let G2 be inducedSubgraph of G,V,E; :: thesis: not G2 is edge-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 edge-finite

hence not G2 is edge-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 edge-finite

then G == G2 by GLIB_000:def 37;
hence not G2 is edge-finite by Th8; :: thesis: verum

end;

end;