for G, G2 being _Graph
for v1, e, v2 being object
for G1 being addAdjVertex of G,v1,e,v2 st G1 == G2 holds
G2 is addAdjVertex of G,v1,e,v2