theorem :: PROB_2:20

for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B, C being Event of Sigma
for P being Probability of Sigma holds
( A,B,C are_independent_respect_to P iff ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & A,B are_independent_respect_to P & B,C are_independent_respect_to P & A,C are_independent_respect_to P ) ) ;