let A be closed-interval Subset of REAL ; :: thesis: ( - sin is_integrable_on A & (- sin ) | A is bounded )
Y: A c= dom (- sin ) by D3;
(- sin ) | A is continuous ;
hence ( - sin is_integrable_on A & (- sin ) | A is bounded ) by Y, INTEGRA5:10, INTEGRA5:11; :: thesis: verum