:: deftheorem Def2 defines sqrt SURREALS:def 2 :
for lamb being object
for X, Y being set
for b₄ being surreal-membered set holds
( b₄ = sqrt (lamb,X,Y) iff for o being object holds
( o in b₄ iff ex x, y being Surreal st
( x in X & y in Y & not x + y == 0_No & o = (lamb +' (x * y)) * ((x + y) ") ) ) );