for a being Real st 1 < a holds
a < a ^2