theorem :: SQUARE_1:42

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