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