:: deftheorem Def7 defines sqrt SURREALS:def 7 :
for o being object st o is Surreal holds
for b₂ being set holds
( b₂ = sqrt o iff for x being Surreal st x = o holds
b₂ = (No_sqrt_op (born x)) . x );