theorem Th25: :: ACKERMAN:25

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