(sigma_Meas (C_Meas M)) | (sigma (Field_generated_by S)) is sigma_Measure of (sigma (Field_generated_by S)) by Th61;
hence ex b₁ being sigma_Measure of (sigma (Field_generated_by S)) st b₁ = (sigma_Meas (C_Meas M)) | (sigma (Field_generated_by S)) ; :: thesis: verum