theorem Th3: :: INTEGR15:3

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_below & 0 < e holds

ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e

for f being Function of A,REAL

for D being Division of A

for e being Real st f | A is bounded_below & 0 < e holds

ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e