for G2 being _Graph
for V being set
for G1 being addLoops of G2,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st not v1 in V & v1 = v2 holds
( ( v1 is isolated implies v2 is isolated ) & ( v2 is isolated implies v1 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v2 is endvertex implies v1 is endvertex ) )