let z1, z2 be Complex; :: thesis: for X being complex-membered set holds (addRel (X,z1)) * (addRel (X,z2)) c= addRel (X,(z1 + z2))
let X be complex-membered set ; :: thesis: (addRel (X,z1)) * (addRel (X,z2)) c= addRel (X,(z1 + z2))

now :: thesis: for x, y being object st [x,y] in (addRel (X,z1)) * (addRel (X,z2)) holds
[x,y] in addRel (X,(z1 + z2))

let x, y be object ; :: thesis: ( [x,y] in (addRel (X,z1)) * (addRel (X,z2)) implies [x,y] in addRel (X,(z1 + z2)) )
assume [x,y] in (addRel (X,z1)) * (addRel (X,z2)) ; :: thesis: [x,y] in addRel (X,(z1 + z2))
then consider z being object such that
A1: ( [x,z] in addRel (X,z1) & [z,y] in addRel (X,z2) ) by RELAT_1:def 8;
reconsider a = x, b = y, c = z as set by TARSKI:1;
( [a,c] in addRel (X,z1) & [c,b] in addRel (X,z2) ) by A1;
then A2: ( a in X & c in X & b in X ) by MMLQUER2:4;
then reconsider a = a, b = b, c = c as Complex ;
( c = z1 + a & b = z2 + c ) by A1, Th11;
then b = (z1 + z2) + a ;
hence [x,y] in addRel (X,(z1 + z2)) by A2, Th11; :: thesis: verum

end;

hence (addRel (X,z1)) * (addRel (X,z2)) c= addRel (X,(z1 + z2)) by RELAT_1:def 3; :: thesis: verum