theorem :: MEASURE3:12

for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for F being sequence of S st ( for n being Nat holds F . (n + 1) c= F . n ) & M . (F . 0) < +infty holds
M . (meet (rng F)) = inf (rng (M * F))