let x, y be Surreal; :: thesis: ( 0_No <= x & x <= y implies sqrt x <= sqrt y )
assume that
A1: ( 0_No <= x & x <= y ) and
A2: sqrt y < sqrt x ; :: thesis: contradiction
A3: ( 0_No <= sqrt x & (sqrt x) * (sqrt x) == x ) by A1, Th19;
0_No <= y by A1, SURREALO:4;
then A4: ( 0_No <= sqrt y & (sqrt y) * (sqrt y) == y ) by Th19;
0_No < sqrt x by A4, A2, SURREALO:4;
then (sqrt y) * (sqrt x) < (sqrt x) * (sqrt x) by A2, SURREALR:70;
then A5: (sqrt y) * (sqrt x) < x by A3, SURREALO:4;
sqrt y <= sqrt x by A2;
then (sqrt y) * (sqrt y) <= (sqrt x) * (sqrt y) by A4, SURREALR:75;
then y <= (sqrt x) * (sqrt y) by A4, SURREALO:4;
hence contradiction by A1, A5, SURREALO:4; :: thesis: verum