let E be non empty finite set ; :: thesis: for A, B being Event of E holds prob A = (prob (A /\ B)) + (prob (A /\ (B `)))
let A, B be Event of E; :: thesis: prob A = (prob (A /\ B)) + (prob (A /\ (B `)))
A = A /\ (A \/ ([#] E)) by XBOOLE_1:21;
then A = A /\ ([#] E) by SUBSET_1:11;
then A1: A = A /\ (B \/ (B `)) by SUBSET_1:10;
prob ((A /\ B) \/ (A /\ (B `))) = (prob (A /\ B)) + (prob (A /\ (B `))) by Th13, Th21;
hence prob A = (prob (A /\ B)) + (prob (A /\ (B `))) by A1, XBOOLE_1:23; :: thesis: verum