let G1 be addAdjVertexAll of G, the_Vertices_of G,V; :: thesis: not G1 is locally-finite
A1: not the_Vertices_of G in the_Vertices_of G ;
then reconsider v = the_Vertices_of G as Vertex of G1 by GLIB_007:50;
v .degree() = card V by A1, GLIBPRE0:57;
hence not G1 is locally-finite by Th23; :: thesis: verum