theorem Th39: :: INTEGRA8:39

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