let p be Real; :: thesis: cosh . p >= 1
((exp_R . p) + (exp_R . (- p))) / 2 >= 2 / 2 by Lm24, XREAL_1:72;
hence cosh . p >= 1 by Def3; :: thesis: verum