:: deftheorem Def10 defines induced_sigma_Measure MEASURE9:def 9 :
for X being non empty set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for M being induced_Measure of S,P
for b₅ being sigma_Measure of (sigma (Field_generated_by S)) holds
( b₅ is induced_sigma_Measure of S,M iff b₅ = (sigma_Meas (C_Meas M)) | (sigma (Field_generated_by S)) );