theorem Th15: :: SQUARE_1:15

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