theorem Th27: :: ACKERMAN:27
for r, n being Nat holds Ackermann (r,(n + n)) < Ackermann ((r + 4),n)