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