for r being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded & r <= 0 holds
(upper_sum_set (r (#) f)) . D >= (r * (upper_bound (rng f))) * (vol A)