:: deftheorem Def4 defines MeasPart MEASURE3:def 4 :
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of COM (S,M)
for b₅ being non empty Subset-Family of X holds
( b₅ = MeasPart A iff for B being set holds
( B in b₅ iff ( B in S & B c= A & A \ B is thin of M ) ) );