theorem Th13: :: MEASURE8:13

for X being set
for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)