for a being Real
for n being natural Number st 1 <= a & 1 <= n holds
a <= a |^ n