:: deftheorem Def6 defines Volume MEASURE8:def 6 :
for X being set
for F being Field_Subset of X
for Sets being SetSequence of X
for M being Measure of F
for Cvr being Covering of Sets,F
for b₆ being ExtREAL_sequence holds
( b₆ = Volume (M,Cvr) iff for n being Nat holds b₆ . n = SUM (vol (M,(Cvr . n))) );