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