theorem :: MESFUNC8:5

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 holds
ex G being sequence of S st
( G = inferior_setsequence F & M . (lim F) = sup (rng (M * G)) )