let E be non empty finite set ; :: thesis: for A, B, C being Event of E st A misses B & A misses C & B misses C holds
prob ((A \/ B) \/ C) = ((prob A) + (prob B)) + (prob C)
let A, B, C be Event of E; :: thesis: ( A misses B & A misses C & B misses C implies prob ((A \/ B) \/ C) = ((prob A) + (prob B)) + (prob C) )
assume that
A1: A misses B and
A2: A misses C and
A3: B misses C ; :: thesis: prob ((A \/ B) \/ C) = ((prob A) + (prob B)) + (prob C)
A4: prob (A /\ (B /\ C)) = 0 by A1, Th16, XBOOLE_1:74;
prob ((A \/ B) \/ C) = ((((prob A) + (prob B)) + (prob C)) - (((prob (A /\ B)) + (prob (A /\ C))) + (prob (B /\ C)))) + (prob ((A /\ B) /\ C)) by Th29
.= ((((prob A) + (prob B)) + (prob C)) - (((prob (A /\ B)) + (prob (A /\ C))) + (prob (B /\ C)))) + 0 by A4, XBOOLE_1:16
.= (((prob A) + (prob B)) + (prob C)) - (((prob (A /\ B)) + (prob (A /\ C))) + 0) by A3, Th16
.= (((prob A) + (prob B)) + (prob C)) - ((prob (A /\ B)) + 0) by A2, Th16
.= (((prob A) + (prob B)) + (prob C)) - 0 by A1, Th16 ;
hence prob ((A \/ B) \/ C) = ((prob A) + (prob B)) + (prob C) ; :: thesis: verum