let H be DLGraphComplement of G; :: thesis: not H is vertex-finite
the_Vertices_of H = the_Vertices_of G by GLIB_012:def 6;
hence not H is vertex-finite ; :: thesis: verum