theorem Th7: :: INTEGR15:7

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for T being DivSequence of A

for e being Element of REAL st 0 < e & f | A is bounded_below holds

ex S being middle_volume_Sequence of f,T st

for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e

for f being Function of A,REAL

for T being DivSequence of A

for e being Element of REAL st 0 < e & f | A is bounded_below holds

ex S being middle_volume_Sequence of f,T st

for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e