theorem Th2: :: NAT_3:2

for a, b being Nat st 1 < a holds
b <= a |^ b