theorem Th49: :: ACKERMAN:49

for m, n being Nat st 1 <= n & n <= m holds
AckermannFunction majorizes m succ n