theorem Th90: :: INTEGRA8:90

for A being non empty closed_interval Subset of REAL holds integral ((sin (#) cos),A) = (1 / 2) * (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A))))