let x be real number ; :: thesis: 1 + ((cosh x) + (cosh x)) <> 0
cosh . x > 0 by SIN_COS2:15;
then cosh x > 0 by SIN_COS2:def 4;
hence 1 + ((cosh x) + (cosh x)) <> 0 ; :: thesis: verum