let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B, C being Event of Sigma st A,B,C are_independent_respect_to P holds
A,C,B are_independent_respect_to P
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for A, B, C being Event of Sigma st A,B,C are_independent_respect_to P holds
A,C,B are_independent_respect_to P
let P be Probability of Sigma; :: thesis: for A, B, C being Event of Sigma st A,B,C are_independent_respect_to P holds
A,C,B are_independent_respect_to P
let A, B, C be Event of Sigma; :: thesis: ( A,B,C are_independent_respect_to P implies A,C,B are_independent_respect_to P )
assume A1: A,B,C are_independent_respect_to P ; :: thesis: A,C,B are_independent_respect_to P
then P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) by Th32;
then A2: P . ((A /\ C) /\ B) = ((P . A) * (P . C)) * (P . B) by XBOOLE_1:16;
B,C are_independent_respect_to P by A1, Th32;
then A3: C,B are_independent_respect_to P by Th31;
( A,B are_independent_respect_to P & A,C are_independent_respect_to P ) by A1, Th32;
hence A,C,B are_independent_respect_to P by A2, A3, Th32; :: thesis: verum