theorem Th30: :: GLIB_013:30

for G1 being non locally-finite _Graph
for V being finite Subset of (the_Vertices_of G1)
for G2 being removeVertices of G1,V st ( for v being Vertex of G1 st v in V holds
v .edgesInOut() is finite ) holds
not G2 is locally-finite