let r, s, y be Nat; :: thesis: (Ackermann (r,y)) + (Ackermann (s,y)) < Ackermann ((4 + (max (r,s))),y)
reconsider z = max (r,s) as Nat by TARSKI:1;
set t = 4 + (max (r,s));
( H₁(r,y) <= H₁(z,y) & H₁(s,y) <= H₁(z,y) ) by Th24, XXREAL_0:25;
then A1: H₁(r,y) + H₁(s,y) <= H₁(z,y) + H₁(z,y) by XREAL_1:7;
(2 * H₁(z,y)) + 3 = H₁(2,H₁(z,y)) by Th10;
then A2: H₁(r,y) + H₁(s,y) < H₁(2,H₁(z,y)) by A1, XXREAL_0:2, NAT_1:16;
H₁(2,H₁(z,y)) < H₁((2 + z) + 2,y) by Th25;
hence (Ackermann (r,y)) + (Ackermann (s,y)) < Ackermann ((4 + (max (r,s))),y) by A2, XXREAL_0:2; :: thesis: verum