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

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