let G2 be _Graph; for v1, e, v2 being object
for G1 being addEdge of G2,v1,e,v2 st v1 <> v2 holds
G1 .loops() = G2 .loops()
let v1, e, v2 be object ; for G1 being addEdge of G2,v1,e,v2 st v1 <> v2 holds
G1 .loops() = G2 .loops()
let G1 be addEdge of G2,v1,e,v2; ( v1 <> v2 implies G1 .loops() = G2 .loops() )
assume A1:
v1 <> v2
; G1 .loops() = G2 .loops()