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, Th41, 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 Th56
.= ((((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, Th41
.= (((prob A) + (prob B)) + (prob C)) - ((prob (A /\ B)) + 0 ) by A2, Th41
.= (((prob A) + (prob B)) + (prob C)) - 0 by A1, Th41 ;
hence prob ((A \/ B) \/ C) = ((prob A) + (prob B)) + (prob C) ; :: thesis: verum