theorem Th36: :: INTEGRA1:38

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_above holds
for i being non zero Element of NAT st i in dom D1 holds
Sum ((upper_volume (f,D1)) | i) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,i)))