theorem Th17: :: ACKERMAN:17

for m, n being Nat holds Ackermann (m,n) < Ackermann (m,(n + 1))