:: deftheorem Def5 defines COM MEASURE3:def 5 :
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for b₄ being sigma_Measure of (COM (S,M)) holds
( b₄ = COM M iff for B being set st B in S holds
for C being thin of M holds b₄ . (B \/ C) = M . B );