theorem :: MEASURE3:14

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