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