theorem :: PREPOWER:15

for a being Real
for n being Nat st 0 < a & a < 1 & 2 <= n holds
a |^ n < a