let G be _Graph; :: thesis: for X, Y being set st X c= Y holds
G .edgesBetween X c= G .edgesBetween Y
let X, Y be set ; :: thesis: ( X c= Y implies G .edgesBetween X c= G .edgesBetween Y )
assume A1: X c= Y ; :: thesis: G .edgesBetween X c= G .edgesBetween Y

now

let x be set ; :: thesis: ( x in G .edgesBetween X implies x in G .edgesBetween Y )
assume A2: x in G .edgesBetween X ; :: thesis: x in G .edgesBetween Y
then ( (the_Source_of G) . x in X & (the_Target_of G) . x in X ) by Lm6;
hence x in G .edgesBetween Y by A1, A2, Lm6; :: thesis: verum

end;

hence G .edgesBetween X c= G .edgesBetween Y by TARSKI:def 3; :: thesis: verum