theorem Th9: :: MEASURE3:9

for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for G, F being sequence of S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Nat holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds
( M . (F . 0) in REAL & inf (rng (M * F)) in REAL & sup (rng (M * G)) in REAL )