:: deftheorem defines vol MEASURE7:def 6 :
for A being Subset of REAL
for F being Interval_Covering of A holds vol F = SUM (F vol);