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-descending holds
M * SSets is non-decreasing