consider y being Surreal such that
A1: ( - 1_No == y & sqrt y < - 1_No & y = [{},{0_No,(((sqrt ((1_No * 1_No) + 1_No)) - 1_No) * ((sqrt ((1_No * 1_No) + 1_No)) - 1_No))}] ) by Th31, SURREALI:def 8;
take y ; :: thesis: ex y being Surreal st
( y == y & y < 0_No & sqrt y < sqrt y )
take - 1_No ; :: thesis: ( y == - 1_No & - 1_No < 0_No & sqrt y < sqrt (- 1_No) )
- 1_No < - 0_No by SURREALI:def 8, SURREALR:10;
hence ( y == - 1_No & - 1_No < 0_No & sqrt y < sqrt (- 1_No) ) by A1; :: thesis: verum