let x, y be Real; :: thesis: ( 0 <= x & x < y implies x ^2 < y ^2 )
assume that
A1: 0 <= x and
A2: x < y ; :: thesis: x ^2 < y ^2
A3: x * y < y * y by A1, A2, XREAL_1:68;
x * x <= x * y by A1, A2, XREAL_1:64;
hence x ^2 < y ^2 by A3, XXREAL_0:2; :: thesis: verum