let G be _Graph; :: thesis: 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

let X, Y be set ; :: thesis: for e, x, y being object st e DJoins x,y,G & x in X & y in Y holds

e DSJoins X,Y,G

let e, x, y be object ; :: thesis: ( e DJoins x,y,G & x in X & y in Y implies e DSJoins X,Y,G )

assume A1: ( e DJoins x,y,G & x in X & y in Y ) ; :: thesis: e DSJoins X,Y,G

then ( e in the_Edges_of G & (the_Source_of G) . e = x & (the_Target_of G) . e = y ) by GLIB_000:def 14;

hence e DSJoins X,Y,G by A1, GLIB_000:def 16; :: thesis: verum

for e, x, y being object st e DJoins x,y,G & x in X & y in Y holds

e DSJoins X,Y,G

let X, Y be set ; :: thesis: for e, x, y being object st e DJoins x,y,G & x in X & y in Y holds

e DSJoins X,Y,G

let e, x, y be object ; :: thesis: ( e DJoins x,y,G & x in X & y in Y implies e DSJoins X,Y,G )

assume A1: ( e DJoins x,y,G & x in X & y in Y ) ; :: thesis: e DSJoins X,Y,G

then ( e in the_Edges_of G & (the_Source_of G) . e = x & (the_Target_of G) . e = y ) by GLIB_000:def 14;

hence e DSJoins X,Y,G by A1, GLIB_000:def 16; :: thesis: verum