theorem Th12: :: INTEGRA5:12

for A being non empty closed_interval Subset of REAL
for X being set
for f being PartFunc of REAL,REAL
for D being Division of A st A c= X & f is_differentiable_on X & (f `| X) | A is bounded holds
( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) )