:: deftheorem Def1 defines Indep KOLMOG01:def 1 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for B being Subset of Sigma
for P being Probability of Sigma
for b₅ being Subset of Sigma holds
( b₅ = Indep (B,P) iff for a being Element of Sigma holds
( a in b₅ iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) );