theorem :: SURREALS:23

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