let x, y be real number ; :: thesis: ( 0 <= x & x <= y implies x ^2 <= y ^2 )
assume ( 0 <= x & x <= y ) ; :: thesis: x ^2 <= y ^2
then ( x * x <= x * y & x * y <= y * y ) by XREAL_1:66;
hence x ^2 <= y ^2 by XXREAL_0:2; :: thesis: verum