:: deftheorem Def4 defines -- SURREALR:def 4 :
for X, b₂ being set holds
( b₂ = -- X iff for o being object holds
( o in b₂ iff ex x being Surreal st
( x in X & o = - x ) ) );