for A being non empty closed_interval Subset of REAL
for D being Division of A holds Sum (lower_volume ((chi (A,A)),D)) = vol A