theorem Th2: :: NAT_6:2

for a being non trivial Nat
for n, m being Nat st n > m holds
a |^ n > a |^ m