theorem Th22: :: GLUNIR00:22

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