theorem Th52: :: GLUNIR00:52

for G being _Graph
for V being set
for H being removeVertices of G,V st V c< the_Vertices_of G holds
VertexAdjSymRel H = (VertexAdjSymRel G) \ ([:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:])