let X be surreal-membered set ; :: thesis: -- (-- X) = X
thus -- (-- X) c= X :: according to XBOOLE_0:def 10 :: thesis: X c= -- (-- X)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in -- (-- X) or x in X )
assume x in -- (-- X) ; :: thesis: x in X
then consider y being Surreal such that
A1: ( y in -- X & x = - y ) by Def4;
ex z being Surreal st
( z in X & y = - z ) by A1, Def4;
hence x in X by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in -- (-- X) )
assume A2: x in X ; :: thesis: x in -- (-- X)
then reconsider x = x as Surreal by SURREAL0:def 16;
- x in -- X by A2, Def4;
then - (- x) in -- (-- X) by Def4;
hence x in -- (-- X) ; :: thesis: verum