theorem Th7: :: GLIB_009:7
for G being _Graph
for X, Y being set
for e, x, y being object st e DJoins x,y,G & x in X & y in Y holds
e DSJoins X,Y,G