let E be non empty finite set ; :: thesis: for A, B being Event of E holds prob (A \/ B) = ((prob A) + (prob B)) - (prob (A /\ B))
let A, B be Event of E; :: thesis: prob (A \/ B) = ((prob A) + (prob B)) - (prob (A /\ B))
set q = (card E) " ;
set p = card E;
card (A \/ B) = ((card A) + (card B)) - (card (A /\ B)) by CARD_2:64;
then (card (A \/ B)) * ((card E) " ) = ((card A) * ((card E) " )) + (((card B) * ((card E) " )) - ((card (A /\ B)) * ((card E) " ))) ;
then (card (A \/ B)) / (card E) = (((card A) * ((card E) " )) + ((card B) * ((card E) " ))) - ((card (A /\ B)) * ((card E) " )) by XCMPLX_0:def 9;
then (card (A \/ B)) / (card E) = (((card A) / (card E)) + ((card B) * ((card E) " ))) - ((card (A /\ B)) * ((card E) " )) by XCMPLX_0:def 9;
then (card (A \/ B)) / (card E) = (((card A) / (card E)) + ((card B) / (card E))) - ((card (A /\ B)) * ((card E) " )) by XCMPLX_0:def 9;
hence prob (A \/ B) = ((prob A) + (prob B)) - (prob (A /\ B)) by XCMPLX_0:def 9; :: thesis: verum