for X being non empty set
for F being Field_Subset of X
for m being Measure of F st ex M being sigma_Measure of (sigma F) st M is_extension_of m holds
m is completely-additive