for X being set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for M being induced_Measure of S,P holds M = (C_Meas M) | (Field_generated_by S)