theorem Th1: :: NAT_6:1

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