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

now

let e be set ; :: thesis: ( e in G .edgesDBetween X1,Y1 implies 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 Def33;
then ( e in the_Edges_of G & (the_Source_of G) . e in X1 & (the_Target_of G) . e in Y1 ) by Def18;
then e DSJoins X2,Y2,G by A1, Def18;
hence e in G .edgesDBetween X2,Y2 by Def33; :: thesis: verum

end;

hence G .edgesDBetween X1,Y1 c= G .edgesDBetween X2,Y2 by TARSKI:def 3; :: thesis: verum