for G1, G2 being _Graph
for X, Y being set
for e, x, y being object st G1 == G2 holds
( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins X,Y,G1 implies e SJoins X,Y,G2 ) & ( e DSJoins X,Y,G1 implies e DSJoins X,Y,G2 ) ) ;