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