for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-ascending holds
M * SSets is non-increasing