let G2 be Subgraph of G; :: thesis: ( G2 is spanning implies not G2 is vertex-finite )
assume G2 is spanning ; :: thesis: not G2 is vertex-finite
then the_Vertices_of G2 = the_Vertices_of G by GLIB_000:def 33;
hence not G2 is vertex-finite ; :: thesis: verum