let x be Surreal; :: thesis: {(- x)} = -- {x}
for o being object st o in {(- x)} holds
o in -- {x}

proof

let o be object ; :: thesis: ( o in {(- x)} implies o in -- {x} )
assume o in {(- x)} ; :: thesis: o in -- {x}
then ( o = - x & x in {x} ) by TARSKI:def 1;
hence o in -- {x} by Def4; :: thesis: verum

end;

hence {(- x)} c= -- {x} by TARSKI:def 3; :: according to XBOOLE_0:def 10 :: thesis: -- {x} c= {(- x)}
let xy be object ; :: according to TARSKI:def 3 :: thesis: ( not xy in -- {x} or xy in {(- x)} )
assume xy in -- {x} ; :: thesis: xy in {(- x)}
then consider y being Surreal such that
A1: ( y in {x} & xy = - y ) by Def4;
x = y by A1, TARSKI:def 1;
hence xy in {(- x)} by A1, TARSKI:def 1; :: thesis: verum