let H be DGraphComplement 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:80;
(the_Vertices_of H) \ {w} = w .inNeighbors() by GLIB_012:96
.= (the_Source_of H) .: (w .edgesIn()) ;
hence not H is edge-finite ; :: thesis: verum