theorem Th4: :: INTEGR15:4

for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F)