theorem Th52: :: ACKERMAN:52

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