theorem Th50: :: ACKERMAN:50

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