:: deftheorem Def9 defines sqrt_0 SURREALS:def 9 :
for x being object
for b₂ being pair set holds
( b₂ = sqrt_0 x iff for o being object holds
( ( o in L_ b₂ implies ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) ) & ( ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) implies o in L_ b₂ ) & ( o in R_ b₂ implies ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) ) & ( ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) implies o in R_ b₂ ) ) );