:: deftheorem Def10 defines -' SURREALR:def 10 :
for x being object st x is surreal holds
for b₂ being Surreal holds
( b₂ = -' x iff for x1 being Surreal st x1 = x holds
b₂ = - x1 );