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