theorem Th25: :: INTEGRA1:27

for A being non empty closed_interval Subset of REAL
for D being Division of A
for f being Function of A,REAL st f | A is bounded_above holds
upper_sum (f,D) <= (upper_bound (rng f)) * (vol A)