let G be _Graph; :: thesis: for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds
G .edgesDBetween (X1,Y1) c= G .edgesDBetween (X2,Y2)
let X1, X2, Y1, Y2 be set ; :: thesis: ( X1 c= X2 & Y1 c= Y2 implies G .edgesDBetween (X1,Y1) c= G .edgesDBetween (X2,Y2) )
assume A1: ( X1 c= X2 & Y1 c= Y2 ) ; :: thesis: G .edgesDBetween (X1,Y1) c= G .edgesDBetween (X2,Y2)
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in G .edgesDBetween (X1,Y1) or e in G .edgesDBetween (X2,Y2) )
assume e in G .edgesDBetween (X1,Y1) ; :: thesis: e in G .edgesDBetween (X2,Y2)
then e DSJoins X1,Y1,G by Def31;
then e DSJoins X2,Y2,G by A1;
hence e in G .edgesDBetween (X2,Y2) by Def31; :: thesis: verum