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