theorem Th28: :: INTEGRA1:30

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 f | A is bounded_above & len D1 = 1 holds
upper_sum (f,D1) >= upper_sum (f,D2)