theorem Th23: :: GLUNIR00:23

for G being non _trivial _Graph
for v being Vertex of G
for H being removeVertex of G,v holds VertexDomRel H = (VertexDomRel G) \ ([:{v},(the_Vertices_of G):] \/ [:(the_Vertices_of G),{v}:])