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;
(sqrt y) * (sqrt x) <= (sqrt x) * (sqrt x) by A3, A2, SURREALR:75;
then A5: (sqrt y) * (sqrt x) <= x by A3, SURREALO:4;
(sqrt y) * (sqrt y) <= (sqrt x) * (sqrt y) by A2, A4, SURREALR:75;
then y <= (sqrt x) * (sqrt y) by A4, SURREALO:4;
hence contradiction by A1, A5, SURREALO:4; :: thesis: verum