for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for F being SetSequence of S st F is convergent & M . (Union F) < +infty holds
ex G being sequence of S st
( G = superior_setsequence F & M . (lim F) = inf (rng (M * G)) ) by Th4;