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;
then (cosh x) + (cosh x) > 0 + 0 ;
hence 1 + ((cosh x) + (cosh x)) <> 0 ; :: thesis: verum