theorem Th1: :: INTEGR15:1

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for D being Division of A

for F being middle_volume of f,D st f | A is bounded_below holds

lower_sum (f,D) <= middle_sum (f,F)

for f being Function of A,REAL

for D being Division of A

for F being middle_volume of f,D st f | A is bounded_below holds

lower_sum (f,D) <= middle_sum (f,F)