let k, m, n be Nat; :: thesis: Ackermann (k,(Ackermann (m,n))) < Ackermann (((k + m) + 2),n)
A1: H₁(k,H₁(m,n)) <= H₁(k + m,H₁(m,n)) by Th24, NAT_1:11;
m < m + (k + 1) by NAT_1:16;
then H₁(m,n) < H₁((k + m) + 1,n) by Th23;
then H₁(k + m,H₁(m,n)) < H₁(k + m,H₁((k + m) + 1,n)) by Th18;
then A2: H₁(k,H₁(m,n)) < H₁(k + m,H₁((k + m) + 1,n)) by A1, XXREAL_0:2;
A3: H₁(k + m,H₁((k + m) + 1,n)) = H₁((k + m) + 1,n + 1) by Th7;
H₁((k + m) + 1,n + 1) <= H₁(((k + m) + 1) + 1,n) by Th21;
hence H₁(k,H₁(m,n)) < H₁((k + m) + 2,n) by A2, A3, XXREAL_0:2; :: thesis: verum