let x be Surreal; :: thesis: ( 0_No <= x implies sqrt (x * x) == x )
set S = sqrt (x * x);
assume that
A1: 0_No <= x and
A2: not sqrt (x * x) == x ; :: thesis: contradiction
A3: 0_No * x <= x * x by A1, SURREALR:75;
0_No * x <= x * x by A1, SURREALR:75;
then A4: ( x == sqrt (x * x) or x == - (sqrt (x * x)) ) by Th28;
then - 0_No <= - (sqrt (x * x)) by A2, A1, SURREALO:4;
then A5: sqrt (x * x) == 0_No by A3, Th19, SURREALR:10;
then - (sqrt (x * x)) == - 0_No by SURREALR:10;
then x == - 0_No by A4, A2, SURREALO:4;
hence contradiction by A2, A5, SURREALO:4; :: thesis: verum