let m, n be Nat; :: thesis: m const n in majorizedBy AckermannFunction
AckermannFunction majorizes m const n by Th43;
hence m const n in majorizedBy AckermannFunction ; :: thesis: verum