let G1 be Supergraph of G; :: thesis: not G1 is vertex-finite
G is Subgraph of G1 by GLIB_006:57;
hence not G1 is vertex-finite ; :: thesis: verum