:: deftheorem Def14 defines " SURREALI:def 14 :
for x being Surreal st not x == 0_No holds
for b₂ being Surreal holds
( ( x is positive implies ( b₂ = x " iff b₂ = inv x ) ) & ( not x is positive implies ( b₂ = x " iff - b₂ = inv (- x) ) ) );