let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for A, B, C being Event of Sigma
for P being Probability of Sigma st A,B are_independent_respect_to P & A,C are_independent_respect_to P & B misses C holds
A,B \/ C are_independent_respect_to P

let Sigma be SigmaField of Omega; :: thesis: for A, B, C being Event of Sigma
for P being Probability of Sigma st A,B are_independent_respect_to P & A,C are_independent_respect_to P & B misses C holds
A,B \/ C are_independent_respect_to P

let A, B, C be Event of Sigma; :: thesis: for P being Probability of Sigma st A,B are_independent_respect_to P & A,C are_independent_respect_to P & B misses C holds
A,B \/ C are_independent_respect_to P

let P be Probability of Sigma; :: thesis: ( A,B are_independent_respect_to P & A,C are_independent_respect_to P & B misses C implies A,B \/ C are_independent_respect_to P )
assume that
A1: A,B are_independent_respect_to P and
A2: A,C are_independent_respect_to P and
A3: B misses C ; :: thesis:
A4: A /\ B misses A /\ C by ;
P . (A /\ (B \/ C)) = P . ((A /\ B) \/ (A /\ C)) by XBOOLE_1:23
.= (P . (A /\ B)) + (P . (A /\ C)) by
.= ((P . A) * (P . B)) + (P . (A /\ C)) by A1
.= ((P . A) * (P . B)) + ((P . A) * (P . C)) by A2
.= (P . A) * ((P . B) + (P . C))
.= (P . A) * (P . (B \/ C)) by ;
hence A,B \/ C are_independent_respect_to P ; :: thesis: verum