let E be non empty finite set ; 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; ( 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
; 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)
; verum