:: deftheorem defines are_independent_respect_to PROB_2:def 4 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being Event of Sigma holds
( A,B are_independent_respect_to P iff P . (A /\ B) = (P . A) * (P . B) );