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

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