let E be non empty finite set ; :: thesis: for A, B being Event of E st A misses B holds
prob (A \/ B) = (prob A) + (prob B)
let A, B be Event of E; :: thesis: ( A misses B implies prob (A \/ B) = (prob A) + (prob B) )
assume A misses B ; :: thesis: prob (A \/ B) = (prob A) + (prob B)
then prob (A /\ B) = 0 by Th41;
then prob (A \/ B) = ((prob A) + (prob B)) - 0 by Th46;
hence prob (A \/ B) = (prob A) + (prob B) ; :: thesis: verum