let a, b, n be Nat; :: thesis: ( a <= b implies Ackermann (a,n) <= Ackermann (b,n) )
assume a <= b ; :: thesis: Ackermann (a,n) <= Ackermann (b,n)
then ( a < b or a = b ) by XXREAL_0:1;
hence Ackermann (a,n) <= Ackermann (b,n) by Th23; :: thesis: verum