let E be non empty finite set ; :: thesis: for A, B, C being Event of E holds prob ((A \/ B) \/ C) = ((((prob A) + (prob B)) + (prob C)) - (((prob (A /\ B)) + (prob (A /\ C))) + (prob (B /\ C)))) + (prob ((A /\ B) /\ C))
let A, B, C be Event of E; :: thesis: prob ((A \/ B) \/ C) = ((((prob A) + (prob B)) + (prob C)) - (((prob (A /\ B)) + (prob (A /\ C))) + (prob (B /\ C)))) + (prob ((A /\ B) /\ C))
prob ((A \/ B) \/ C) = ((prob (A \/ B)) + (prob C)) - (prob ((A \/ B) /\ C)) by Th46
.= ((((prob A) + (prob B)) - (prob (A /\ B))) + (prob C)) - (prob ((A \/ B) /\ C)) by Th46
.= ((((prob A) + (prob B)) + (prob C)) + (- (prob (A /\ B)))) - (prob ((A /\ C) \/ (B /\ C))) by XBOOLE_1:23
.= ((((prob A) + (prob B)) + (prob C)) + (- (prob (A /\ B)))) - (((prob (A /\ C)) + (prob (B /\ C))) - (prob ((A /\ C) /\ (B /\ C)))) by Th46
.= ((((prob A) + (prob B)) + (prob C)) + (- (prob (A /\ B)))) - (((prob (A /\ C)) + (prob (B /\ C))) - (prob (A /\ (C /\ (C /\ B))))) by XBOOLE_1:16
.= ((((prob A) + (prob B)) + (prob C)) + (- (prob (A /\ B)))) - (((prob (A /\ C)) + (prob (B /\ C))) - (prob (A /\ ((C /\ C) /\ B)))) by XBOOLE_1:16
.= ((((prob A) + (prob B)) + (prob C)) + (- (prob (A /\ B)))) - (((prob (A /\ C)) + (prob (B /\ C))) - (prob ((A /\ B) /\ C))) by XBOOLE_1:16
.= ((((prob A) + (prob B)) + (prob C)) + (- (((prob (A /\ B)) + (prob (A /\ C))) + (prob (B /\ C))))) + (prob ((A /\ B) /\ C)) ;
hence prob ((A \/ B) \/ C) = ((((prob A) + (prob B)) + (prob C)) - (((prob (A /\ B)) + (prob (A /\ C))) + (prob (B /\ C)))) + (prob ((A /\ B) /\ C)) ; :: thesis: verum