theorem Th21: :: SURREALS:21

for x being Surreal st 0_No <= x holds
( 0_No <= sqrt x & (sqrt x) * (sqrt x) == x ) by Th19;