let x, y be real number ; :: 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: ( 0 <= sqrt x & 0 <= sqrt y ) by A1, A2, Def4;
( (sqrt x) ^2 = x & (sqrt y) ^2 = y ) by A1, A2, Def4;
hence sqrt x < sqrt y by A2, A3, Th77; :: thesis: verum