:: deftheorem Def7 defines vol MEASURE7:def 7 :
for F being sequence of (bool REAL)
for G being Interval_Covering of F
for b₃ being sequence of ExtREAL holds
( b₃ = vol G iff for n being Element of NAT holds b₃ . n = vol (G . n) );