theorem Th51: :: ACKERMAN:51

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