let X, Y be Subset of REAL ; :: thesis: (- X) + (- Y) = - (X + Y)
A1: - (X + Y) = { (- z) where z is Real : z in X + Y } by PSCOMP_1:def 7;
A2: - X = { (- z) where z is Real : z in X } by PSCOMP_1:def 7;
A3: X + Y = { (x + y) where x, y is Real : ( x in X & y in Y ) } by COMPLSP1:def 21;
A4: - Y = { (- z) where z is Real : z in Y } by PSCOMP_1:def 7;
A5: (- X) + (- Y) = { (x + y) where x, y is Real : ( x in - X & y in - Y ) } by COMPLSP1:def 21;
for z being Real st z in - (X + Y) holds
z in (- X) + (- Y)

proof

let z be Real; :: thesis: ( z in - (X + Y) implies z in (- X) + (- Y) )
assume z in - (X + Y) ; :: thesis: z in (- X) + (- Y)
then consider x being Real such that
A6: z = - x and
A7: x in X + Y by A1;
consider a, b being Real such that
A8: x = a + b and
A9: a in X and
A10: b in Y by A3, A7;
A11: - a in - X by A2, A9;
A12: - b in - Y by A4, A10;
z = (- a) + (- b) by A6, A8;
hence z in (- X) + (- Y) by A5, A11, A12; :: thesis: verum

end;

then A13: - (X + Y) c= (- X) + (- Y) by SUBSET_1:7;
for z being Real st z in (- X) + (- Y) holds
z in - (X + Y)

proof

let z be Real; :: thesis: ( z in (- X) + (- Y) implies z in - (X + Y) )
assume z in (- X) + (- Y) ; :: thesis: z in - (X + Y)
then consider x, y being Real such that
A14: z = x + y and
A15: x in - X and
A16: y in - Y by A5;
consider b being Real such that
A17: y = - b and
A18: b in Y by A4, A16;
consider a being Real such that
A19: x = - a and
A20: a in X by A2, A15;
A21: a + b in X + Y by A3, A20, A18;
z = - (a + b) by A14, A19, A17;
hence z in - (X + Y) by A1, A21; :: thesis: verum

end;

then (- X) + (- Y) c= - (X + Y) by SUBSET_1:7;
hence (- X) + (- Y) = - (X + Y) by A13, XBOOLE_0:def 10; :: thesis: verum