:: deftheorem Def3 defines sigma_Meas MEASURE4:def 3 :
for X being set
for C being C_Measure of X
for b₃ being Function of (sigma_Field C),ExtREAL holds
( b₃ = sigma_Meas C iff for A being Subset of X st A in sigma_Field C holds
b₃ . A = C . A );