:: deftheorem defines sqrt SURREALS:def 8 :
for x being Surreal holds sqrt x = (No_sqrt_op (born x)) . x;