let X, Y be Subset of REAL; :: thesis: (-- X) ++ (-- Y) = -- (X ++ Y)
for z being set st z in -- (X ++ Y) holds
z in (-- X) ++ (-- Y)

proof

let z be set ; :: thesis: ( z in -- (X ++ Y) implies z in (-- X) ++ (-- Y) )
assume Y: z in -- (X ++ Y) ; :: thesis: z in (-- X) ++ (-- Y)
reconsider XY = X ++ Y as Subset of REAL by MEMBERED:3;
z in -- XY by Y;
then consider x being Real such that
A7: x in XY and
A6: z = - x by MEASURE6:108;
consider a, b being Real such that
A9: a in X and
A10: b in Y and
A8: x = a + b by A7, MEASURE6:57;
A11: - a in -- X by A9, MEMBER_1:11;
A12: - b in -- Y by A10, MEMBER_1:11;
z = (- a) + (- b) by A6, A8;
hence z in (-- X) ++ (-- Y) by A11, A12, MEMBER_1:46; :: thesis: verum

end;

then A13: -- (X ++ Y) c= (-- X) ++ (-- Y) by TARSKI:def 3;
for z being set st z in (-- X) ++ (-- Y) holds
z in -- (X ++ Y)

proof

let z be set ; :: thesis: ( z in (-- X) ++ (-- Y) implies z in -- (X ++ Y) )
assume AA: z in (-- X) ++ (-- Y) ; :: thesis: z in -- (X ++ Y)
(-- X) ++ (-- Y) c= REAL by MEMBERED:3;
then z in REAL by AA;
then consider x, y being Real such that
A15: x in -- X and
A16: y in -- Y and
A14: z = x + y by AA, MEASURE6:57;
consider b being Real such that
A18: b in Y and
A17: y = - b by A16, MEASURE6:108;
reconsider X = X as Subset of REAL ;
consider a being Real such that
A20: a in X and
A19: x = - a by A15, MEASURE6:108;
A21: a + b in X ++ Y by A20, A18, MEMBER_1:46;
z = - (a + b) by A14, A19, A17;
hence z in -- (X ++ Y) by A21, MEMBER_1:11; :: thesis: verum

end;

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