:: deftheorem Def8 defines COM PROB_4:def 8 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for b₄ being Probability of COM (Sigma,P) holds
( b₄ = COM P iff for B being set st B in Sigma holds
for C being thin of P holds b₄ . (B \/ C) = P . B );