let H be DLGraphComplement of G; :: thesis: not H is edge-finite
set v = the isolated Vertex of G;
reconsider w = the isolated Vertex of G as Vertex of H by GLIB_012:def 6;
the_Vertices_of H = w .inNeighbors() by GLIB_012:61
.= (the_Source_of H) .: (w .edgesIn()) ;
hence not H is edge-finite ; :: thesis: verum