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 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 ) )
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for A, B, C being Event 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 ) )
let P be Probability of Sigma; :: thesis: for A, B, C being Event 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 ) )
let A, B, C be Event of Sigma; :: thesis: ( 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 ) )
thus ( A,B,C are_independent_respect_to P implies ( 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 ) ) :: thesis: ( 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 implies A,B,C are_independent_respect_to P )

proof

assume A,B,C are_independent_respect_to P ; :: thesis: ( 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 )
then ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & P . (A /\ B) = (P . A) * (P . B) & P . (A /\ C) = (P . A) * (P . C) & P . (B /\ C) = (P . B) * (P . C) ) by Def6;
hence ( 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 ) by Def5; :: thesis: verum

end;

assume ( 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 ) ; :: thesis: A,B,C are_independent_respect_to P
then ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & P . (A /\ B) = (P . A) * (P . B) & P . (A /\ C) = (P . A) * (P . C) & P . (B /\ C) = (P . B) * (P . C) ) by Def5;
hence A,B,C are_independent_respect_to P by Def6; :: thesis: verum