theorem Th46: :: INTEGRA8:46

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