theorem Th5: :: MEASURE8:5

for X being set
for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X
for n being Nat
for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n