theorem Th29: :: GLIB_013:29

for G2 being _Graph
for v being object
for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V st not v in the_Vertices_of G2 holds
( ( G2 is locally-finite & V is finite ) iff G1 is locally-finite )