theorem Th19: :: SURREALS:19

for x, y being Surreal st 0_No <= x holds
( ( y = sqrt x implies ( 0_No <= y & y * y == x & ( x == 0_No implies y == 0_No ) & ( 0_No < x implies 0_No < y ) ) ) & ( y in L_ (sqrt x) implies ( 0_No <= y & y * y < x ) ) & ( y in R_ (sqrt x) implies ( 0_No < y & x < y * y ) ) & sqrt x is surreal )