theorem Th16: :: SQUARE_1:16

for x, y being Real st 0 <= x & x < y holds
x ^2 < y ^2