theorem Th5: :: INTEGR15:5

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for T being DivSequence of A

for S being middle_volume_Sequence of f,T

for i being Element of NAT st f | A is bounded_below holds

(lower_sum (f,T)) . i <= (middle_sum (f,S)) . i

for f being Function of A,REAL

for T being DivSequence of A

for S being middle_volume_Sequence of f,T

for i being Element of NAT st f | A is bounded_below holds

(lower_sum (f,T)) . i <= (middle_sum (f,S)) . i