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:45;
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