let y be object ; :: according to SURREAL0:def 16 :: thesis: ( not y in -- X or y is surreal )
assume y in -- X ; :: thesis: y is surreal
then ex x being Surreal st
( x in X & y = - x ) by Def4;
hence y is surreal ; :: thesis: verum