for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL
for B being Real st 0 < vol A & ( for D being Division of A
for K being var_volume of rho,D st lower_bound A < D . 1 holds
Sum K <= B ) holds
for D being Division of A
for K being var_volume of rho,D holds Sum K <= B