let x be Real; :: 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