let H be GraphComplement of G; :: thesis: not H is vertex-finite
the_Vertices_of H = the_Vertices_of G by GLIB_012:98;
hence not H is vertex-finite ; :: thesis: verum