let x, y be Real; :: thesis: ( 0 <= x & x <= y implies sqrt x <= sqrt y )

per cases ( x = y or x <> y ) ;

suppose x = y ; :: thesis: ( 0 <= x & x <= y implies sqrt x <= sqrt y )

hence ( 0 <= x & x <= y implies sqrt x <= sqrt y ) ; :: thesis: verum

end;

suppose A1: x <> y ; :: thesis: ( 0 <= x & x <= y implies sqrt x <= sqrt y )

assume A2: 0 <= x ; :: thesis: ( not x <= y or sqrt x <= sqrt y )
assume x <= y ; :: thesis: sqrt x <= sqrt y
then x < y by A1, XXREAL_0:1;
hence sqrt x <= sqrt y by A2, Lm3; :: thesis: verum

end;

end;