theorem Th1: :: NAT_6:1

for a being positive Nat
for n, m being Nat st n >= m holds
a |^ n >= a |^ m