:: deftheorem Def2 defines sigma_Field MEASURE4:def 2 :
for X being set
for C being C_Measure of X
for b₃ being non empty Subset-Family of X holds
( b₃ = sigma_Field C iff for A being Subset of X holds
( A in b₃ iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) );