for G being _Graph
for v being object
for V being set
for G1, G2 being addAdjVertexAll of G,v,V
for v1, e1, v2 being object st e1 Joins v1,v2,G1 holds
ex e2 being object st e2 Joins v1,v2,G2