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

proof

let z be object ; :: thesis: ( z in -- (X ++ Y) implies z in (-- X) ++ (-- Y) )
assume A1: z in -- (X ++ Y) ; :: thesis: z in (-- X) ++ (-- Y)
reconsider XY = X ++ Y as Subset of REAL by MEMBERED:3;
z in -- XY by A1;
then consider x being Real such that
A2: x in XY and
A3: z = - x by MEASURE6:72;
consider a, b being Real such that
A4: a in X and
A5: b in Y and
A6: x = a + b by A2, MEASURE6:21;
A7: - a in -- X by A4, MEMBER_1:11;
A8: - b in -- Y by A5, MEMBER_1:11;
z = (- a) + (- b) by A3, A6;
hence z in (-- X) ++ (-- Y) by A7, A8, MEMBER_1:46; :: thesis: verum

end;

then A9: -- (X ++ Y) c= (-- X) ++ (-- Y) ;
for z being object st z in (-- X) ++ (-- Y) holds
z in -- (X ++ Y)

proof

let z be object ; :: thesis: ( z in (-- X) ++ (-- Y) implies z in -- (X ++ Y) )
assume A10: z in (-- X) ++ (-- Y) ; :: thesis: z in -- (X ++ Y)
consider x, y being Real such that
A11: x in -- X and
A12: y in -- Y and
A13: z = x + y by A10, MEASURE6:21;
consider b being Real such that
A14: b in Y and
A15: y = - b by A12, MEASURE6:72;
reconsider X = X as Subset of REAL ;
consider a being Real such that
A16: a in X and
A17: x = - a by A11, MEASURE6:72;
A18: a + b in X ++ Y by A16, A14, MEMBER_1:46;
z = - (a + b) by A13, A17, A15;
hence z in -- (X ++ Y) by A18, MEMBER_1:11; :: thesis: verum

end;

then (-- X) ++ (-- Y) c= -- (X ++ Y) ;
hence (-- X) ++ (-- Y) = -- (X ++ Y) by A9; :: thesis: verum