theorem Th44: :: INTEGRA1:46

for A being non empty closed_interval Subset of REAL
for D1, D2 being Division of A
for f being Function of A,REAL st D1 <= D2 & f | A is bounded_below holds
lower_sum (f,D2) >= lower_sum (f,D1)