let A be closed-interval Subset of REAL ; :: thesis: ( A = [.0 ,((PI * 3) / 2).] implies integral cos ,A = - 1 )
assume A = [.0 ,((PI * 3) / 2).] ; :: thesis: integral cos ,A = - 1
then ( upper_bound A = (PI * 3) / 2 & lower_bound A = 0 ) by Th37;
then integral cos ,A = (- 1) - (sin . 0 ) by Th39, SIN_COS:81
.= (- 1) - (sin . (0 + (2 * PI ))) by SIN_COS:83
.= (- 1) - 0 by SIN_COS:81 ;
hence integral cos ,A = - 1 ; :: thesis: verum