for G being _Graph
for v1, e, v2 being object
for G1, G2 being addEdge of G,v1,e,v2 holds G1 == G2