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
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in G .edgesBetween X or 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 Lm5;
hence x in G .edgesBetween Y by A1, A2, Lm5; :: thesis: verum