theorem Th2: :: NAT_3:2

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