:: deftheorem Def5 defines COM PROB_4:def 5 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for b₄ being non empty Subset-Family of Omega holds
( b₄ = COM (Sigma,P) iff for A being set holds
( A in b₄ iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) );