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 xy be object ; :: according to TARSKI:def 3 :: thesis: ( not xy in -- (X1 \/ X2) or xy in (-- X1) \/ (-- X2) )
assume xy in -- (X1 \/ X2) ; :: thesis: xy in (-- X1) \/ (-- X2)
then consider x being Surreal such that
A1: ( x in X1 \/ X2 & xy = - x ) by Def4;
( x in X1 or x in X2 ) by A1, XBOOLE_0:def 3;
then ( xy in -- X1 or xy in -- X2 ) by A1, Def4;
hence xy in (-- X1) \/ (-- X2) by XBOOLE_0:def 3; :: thesis: verum

end;

let xy be object ; :: according to TARSKI:def 3 :: thesis: ( not xy in (-- X1) \/ (-- X2) or xy in -- (X1 \/ X2) )
assume xy in (-- X1) \/ (-- X2) ; :: thesis: xy in -- (X1 \/ X2)

per cases then ( xy in -- X1 or xy in -- X2 ) by XBOOLE_0:def 3;

suppose xy in -- X1 ; :: thesis: xy in -- (X1 \/ X2)

then consider x being Surreal such that
A2: ( x in X1 & xy = - x ) by Def4;
x in X1 \/ X2 by A2, XBOOLE_0:def 3;
hence xy in -- (X1 \/ X2) by A2, Def4; :: thesis: verum

end;

suppose xy in -- X2 ; :: thesis: xy in -- (X1 \/ X2)

then consider x being Surreal such that
A3: ( x in X2 & xy = - x ) by Def4;
x in X1 \/ X2 by A3, XBOOLE_0:def 3;
hence xy in -- (X1 \/ X2) by A3, Def4; :: thesis: verum

end;

end;