let A be non empty closed_interval Subset of REAL; :: thesis: ( A = [.0,PI.] implies integral ((- sin),A) = - 2 )
assume A = [.0,PI.] ; :: thesis: integral ((- sin),A) = - 2
then ( upper_bound A = PI & lower_bound A = 0 ) by Th37;
then integral ((- sin),A) = (- 1) - (cos . 0) by Th46, SIN_COS:76
.= (- 1) - (sin . ((PI / 2) - 0)) by SIN_COS:78
.= (- 1) - 1 by SIN_COS:76 ;
hence integral ((- sin),A) = - 2 ; :: thesis: verum