let G be _Graph; :: thesis: for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds
G .edgesBetween (X1,Y1) c= G .edgesBetween (X2,Y2)
let X1, X2, Y1, Y2 be set ; :: thesis: ( X1 c= X2 & Y1 c= Y2 implies G .edgesBetween (X1,Y1) c= G .edgesBetween (X2,Y2) )
assume A1: ( X1 c= X2 & Y1 c= Y2 ) ; :: thesis: G .edgesBetween (X1,Y1) c= G .edgesBetween (X2,Y2)

now :: thesis: for e being set st e in G .edgesBetween (X1,Y1) holds
e in G .edgesBetween (X2,Y2)

let e be set ; :: thesis: ( e in G .edgesBetween (X1,Y1) implies e in G .edgesBetween (X2,Y2) )
assume A2: e in G .edgesBetween (X1,Y1) ; :: thesis: e in G .edgesBetween (X2,Y2)
then e SJoins X1,Y1,G by Def30;
then ( ( (the_Source_of G) . e in X1 & (the_Target_of G) . e in Y1 ) or ( (the_Source_of G) . e in Y1 & (the_Target_of G) . e in X1 ) ) by Def15;
then e SJoins X2,Y2,G by A1, A2, Def15;
hence e in G .edgesBetween (X2,Y2) by Def30; :: thesis: verum

end;

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