for X being set
for F being Field_Subset of X
for M being Measure of F st M is completely-additive holds
for A being set st A in F holds
M . A = (C_Meas M) . A