assume -- {} <> {} ; :: thesis: contradiction
then consider x being object such that
A1: x in -- {} by XBOOLE_0:def 1;
ex y being Surreal st
( y in {} & x = - y ) by A1, Def4;
hence contradiction ; :: thesis: verum