theorem :: ACKERMAN:26

for r, s, y being Nat holds (Ackermann (r,y)) + (Ackermann (s,y)) < Ackermann ((4 + (max (r,s))),y)