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