theorem :: GLUNIR00:61

for G being _Graph
for V being Subset of (the_Vertices_of G)
for H being addLoops of G,V holds VertexAdjSymRel H = (VertexAdjSymRel G) \/ (id V)