let m, n be Nat; :: thesis: ( 1 <= n & n <= m implies m succ n in majorizedBy AckermannFunction )
assume ( 1 <= n & n <= m ) ; :: thesis: m succ n in majorizedBy AckermannFunction
then AckermannFunction majorizes m succ n by Th49;
hence m succ n in majorizedBy AckermannFunction ; :: thesis: verum