for A being non empty closed_interval Subset of REAL
for D being Division of A
for n, k being Nat st D divide_into_equal n & k in dom D holds
vol (divset (D,k)) = (vol A) / n