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 holds P . ((A \/ B) \/ C) = ((((P . A) + (P . B)) + (P . C)) - (((P . (A /\ B)) + (P . (B /\ C))) + (P . (A /\ C)))) + (P . ((A /\ B) /\ C))
let Sigma be SigmaField of Omega; :: thesis: for A, B, C being Event of Sigma
for P being Probability of Sigma holds P . ((A \/ B) \/ C) = ((((P . A) + (P . B)) + (P . C)) - (((P . (A /\ B)) + (P . (B /\ C))) + (P . (A /\ C)))) + (P . ((A /\ B) /\ C))
let A, B, C be Event of Sigma; :: thesis: for P being Probability of Sigma holds P . ((A \/ B) \/ C) = ((((P . A) + (P . B)) + (P . C)) - (((P . (A /\ B)) + (P . (B /\ C))) + (P . (A /\ C)))) + (P . ((A /\ B) /\ C))
let P be Probability of Sigma; :: thesis: P . ((A \/ B) \/ C) = ((((P . A) + (P . B)) + (P . C)) - (((P . (A /\ B)) + (P . (B /\ C))) + (P . (A /\ C)))) + (P . ((A /\ B) /\ C))
A1: P . ((A \/ B) /\ C) = P . ((A /\ C) \/ (B /\ C)) by XBOOLE_1:23
.= ((P . (A /\ C)) + (P . (B /\ C))) - (P . ((A /\ C) /\ (B /\ C))) by PROB_1:38
.= ((P . (A /\ C)) + (P . (B /\ C))) - (P . (A /\ ((B /\ C) /\ C))) by XBOOLE_1:16
.= ((P . (A /\ C)) + (P . (B /\ C))) - (P . (A /\ (B /\ (C /\ C)))) by XBOOLE_1:16
.= ((P . (B /\ C)) + (P . (A /\ C))) - (P . ((A /\ B) /\ C)) by XBOOLE_1:16 ;
P . ((A \/ B) \/ C) = ((P . (A \/ B)) + (P . C)) - (P . ((A \/ B) /\ C)) by PROB_1:38
.= ((((P . A) + (P . B)) - (P . (A /\ B))) + (P . C)) - (P . ((A \/ B) /\ C)) by PROB_1:38
.= (((P . A) + (P . B)) + (P . C)) - ((P . (A /\ B)) + (P . ((A \/ B) /\ C))) ;
hence P . ((A \/ B) \/ C) = ((((P . A) + (P . B)) + (P . C)) - (((P . (A /\ B)) + (P . (B /\ C))) + (P . (A /\ C)))) + (P . ((A /\ B) /\ C)) by A1; :: thesis: verum