for G2 being _Graph
for V being set
for G1 being addVertices of G2,V
for x, y being set
for e being object holds
( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )