theorem :: GLUNIR00:53

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