theorem :: PREPOWER:13

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