for X being set
for S being SigmaField of X
for M being Measure of S
for F being Sep_Sequence of S holds SUM (M * F) <= M . (union (rng F))