let z be Complex; :: thesis: for X, Y being complex-membered set st X c= Y holds
addRel (X,z) c= addRel (Y,z)
let X, Y be complex-membered set ; :: thesis: ( X c= Y implies addRel (X,z) c= addRel (Y,z) )
assume A1: X c= Y ; :: thesis: addRel (X,z) c= addRel (Y,z)

now :: thesis: for x, y being object st [x,y] in addRel (X,z) holds
[x,y] in addRel (Y,z)

let x, y be object ; :: thesis: ( [x,y] in addRel (X,z) implies [x,y] in addRel (Y,z) )
reconsider a = x, b = y as set by TARSKI:1;
assume A2: [x,y] in addRel (X,z) ; :: thesis: [x,y] in addRel (Y,z)
then [a,b] in addRel (X,z) ;
then ( a in X & b in X ) by MMLQUER2:4;
then reconsider a = a, b = b as Complex ;
[a,b] in addRel (X,z) by A2;
then ( a in X & b in X & b = z + a ) by Th11;
hence [x,y] in addRel (Y,z) by A1, Th11; :: thesis: verum

end;

hence addRel (X,z) c= addRel (Y,z) by RELAT_1:def 3; :: thesis: verum