theorem Th39: :: INTEGRA1:41

for i being Element of NAT
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 & i in dom D1 & f | A is bounded_below holds
(PartSums (lower_volume (f,D1))) . i <= (PartSums (lower_volume (f,D2))) . (indx (D2,D1,i))