:: deftheorem Def4 defines vol MEASURE7:def 4 :
for A being Subset of REAL
for F being Interval_Covering of A
for b₃ being sequence of ExtREAL holds
( b₃ = F vol iff for n being Element of NAT holds b₃ . n = diameter (F . n) );