for I being non empty closed_interval Subset of REAL
for D being Division of I
for fc being Function of I,REAL ex i being Nat st
( i in dom D & min (rng (upper_volume (fc,D))) = (upper_volume (fc,D)) . i )