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