let X1, X2 be set ; :: thesis: -- (X1 ++ X2) = (-- X1) ++ (-- X2)
thus -- (X1 ++ X2) c= (-- X1) ++ (-- X2) :: according to XBOOLE_0:def 10 :: thesis: (-- X1) ++ (-- X2) c= -- (X1 ++ X2)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in -- (X1 ++ X2) or a in (-- X1) ++ (-- X2) )
assume a in -- (X1 ++ X2) ; :: thesis: a in (-- X1) ++ (-- X2)
then consider xy being Surreal such that
A1: ( xy in X1 ++ X2 & a = - xy ) by Def4;
consider x, y being Surreal such that
A2: ( x in X1 & y in X2 & xy = x + y ) by A1, Def8;
( - x in -- X1 & - y in -- X2 ) by A2, Def4;
then ( - (x + y) = (- x) + (- y) & (- x) + (- y) in (-- X1) ++ (-- X2) ) by Th40, Def8;
hence a in (-- X1) ++ (-- X2) by A1, A2; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (-- X1) ++ (-- X2) or a in -- (X1 ++ X2) )
assume a in (-- X1) ++ (-- X2) ; :: thesis: a in -- (X1 ++ X2)
then consider x1, y1 being Surreal such that
A3: ( x1 in -- X1 & y1 in -- X2 & a = x1 + y1 ) by Def8;
consider x being Surreal such that
A4: ( x in X1 & x1 = - x ) by A3, Def4;
consider y being Surreal such that
A5: ( y in X2 & y1 = - y ) by A3, Def4;
x + y in X1 ++ X2 by A4, A5, Def8;
then ( (- x) + (- y) = - (x + y) & - (x + y) in -- (X1 ++ X2) ) by Th40, Def4;
hence a in -- (X1 ++ X2) by A3, A4, A5; :: thesis: verum