theorem :: GLIB_009:53

for G2 being _Graph
for v1, e, v2 being object
for G1 being addEdge of G2,v1,e,v2 st v1 <> v2 holds
G1 .loops() = G2 .loops()