theorem :: GLUNIR00:48

for G being _Graph
for H being SimpleGraph of G holds VertexAdjSymRel H = (VertexAdjSymRel G) \ (id (the_Vertices_of G))