theorem Th28: :: SURREALS:28

for x, y being Surreal st 0_No <= x & x == y * y & not y == sqrt x holds
y == - (sqrt x)