theorem Th6: :: MEASURE8:6

for X being set
for F being Field_Subset of X
for M being Measure of F
for k being Nat ex m being Nat st
for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . k <= (Partial_Sums (Volume (M,Cvr))) . m