let H be GraphComplement 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:98;
(the_Vertices_of H) \ {w} = w .allNeighbors() by GLIB_012:119
.= (w .inNeighbors()) \/ (w .outNeighbors()) ;
hence not H is edge-finite ; :: thesis: verum