theorem Th2: :: NAT_6:2
for a being non trivial natural number
for n, m being natural number st n > m holds
a |^ n > a |^ m