let z be Complex; :: thesis: for X being complex-membered set holds (addRel (X,z)) ~ = addRel (X,(- z))
let X be complex-membered set ; :: thesis: (addRel (X,z)) ~ = addRel (X,(- z))

now :: thesis: for x, y being object holds
( ( [x,y] in addRel (X,(- z)) implies [y,x] in addRel (X,z) ) & ( [y,x] in addRel (X,z) implies [x,y] in addRel (X,(- z)) ) )

let x, y be object ; :: thesis: ( ( [x,y] in addRel (X,(- z)) implies [y,x] in addRel (X,z) ) & ( [y,x] in addRel (X,z) implies [x,y] in addRel (X,(- z)) ) )
reconsider a = x, b = y as set by TARSKI:1;

hereby :: thesis: ( [y,x] in addRel (X,z) implies [x,y] in addRel (X,(- z)) )

assume A1: [x,y] in addRel (X,(- z)) ; :: thesis: [y,x] in addRel (X,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 A1;
then ( a in X & b in X & b = (- z) + a ) by Th11;
then ( a in X & b in X & a = z + b ) ;
hence [y,x] in addRel (X,z) by Th11; :: thesis: verum

end;

assume A2: [y,x] in addRel (X,z) ; :: thesis: [x,y] in addRel (X,(- z))
then [b,a] in addRel (X,z) ;
then ( a in X & b in X ) by MMLQUER2:4;
then reconsider a = a, b = b as Complex ;
[b,a] in addRel (X,z) by A2;
then ( a in X & b in X & a = z + b ) by Th11;
then ( a in X & b in X & b = (- z) + a ) ;
hence [x,y] in addRel (X,(- z)) by Th11; :: thesis: verum

end;

hence (addRel (X,z)) ~ = addRel (X,(- z)) by RELAT_1:def 7; :: thesis: verum