theorem :: SQUARE_1:45

for a being Real st - 1 >= a holds
- a <= a ^2