theorem Th9: :: MEASURE8:9

for X being set
for F being Field_Subset of X
for M being Measure of F
for A being set st A in F holds
(C_Meas M) . A <= M . A