theorem Th47: :: GLUNIR00:47

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