theorem :: SURREALS:24

for x being Surreal st x < 0_No & ( for y being Surreal st y in R_ x holds
y < 0_No ) holds
sqrt x = 0_No