:: deftheorem Def3 defines COM MEASURE3:def 3 :
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for b₄ being non empty Subset-Family of X holds
( b₄ = COM (S,M) iff for A being set holds
( A in b₄ iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ) );