let x, y be Real; :: thesis: ( 0 <= x & x < y implies sqrt x < sqrt y )
assume that
A1: 0 <= x and
A2: x < y ; :: thesis: sqrt x < sqrt y
A3: (sqrt y) ^2 = y by A1, A2, Def2;
A4: (sqrt x) ^2 = x by A1, Def2;
0 <= sqrt y by A1, A2, Def2;
hence sqrt x < sqrt y by A2, A4, A3, Th15; :: thesis: verum