let p be real number ; :: thesis: cosh . p >= 1
(exp_R . p) + (exp_R . (- p)) >= 2 by Lm25;
then ((exp_R . p) + (exp_R . (- p))) / 2 >= 2 / 2 by XREAL_1:74;
hence cosh . p >= 1 by Def3; :: thesis: verum