theorem Th31: :: SURREALS:31

for x being Surreal st 0_No < x holds
ex y being Surreal st
( - 1_No == y & sqrt y < - x & y = [{},{0_No,(((sqrt ((x * x) + 1_No)) - x) * ((sqrt ((x * x) + 1_No)) - x))}] )