theorem :: MEASURE4:16
for X being set
for C being C_Measure of X holds sigma_Meas C is_complete sigma_Field C