let x be Real; :: thesis: ( (cosh x) + 1 > 0 & (cosh x) - 1 >= 0 & ((cosh x) + 2) + (cosh x) <> 0 )
cosh . x > 0 by SIN_COS2:15;
then A1: cosh x > 0 by SIN_COS2:def 4;
cosh x >= 1 by Lm1;
then (cosh x) - 1 >= 1 - 1 by XREAL_1:13;
hence ( (cosh x) + 1 > 0 & (cosh x) - 1 >= 0 & ((cosh x) + 2) + (cosh x) <> 0 ) by A1; :: thesis: verum