let A be non empty closed_interval Subset of REAL; :: thesis: ( cosh is_integrable_on A & cosh | A is bounded )
cosh | A is continuous by Lm16;
hence ( cosh is_integrable_on A & cosh | A is bounded ) by Lm10, INTEGRA5:10, INTEGRA5:11; :: thesis: verum