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, XREAL_1:70;
hence x ^2 < y ^2 by XXREAL_0:2; :: thesis: verum