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 ` )))
A1: prob ((A /\ B) \/ (A /\ (B ` ))) = (prob (A /\ B)) + (prob (A /\ (B ` ))) by Th34, Th47;
A = A /\ (A \/ ([#] E)) by XBOOLE_1:21;
then A = A /\ ([#] E) by SUBSET_1:28;
then A = A /\ (B \/ (B ` )) by SUBSET_1:25;
hence prob A = (prob (A /\ B)) + (prob (A /\ (B ` ))) by A1, XBOOLE_1:23; :: thesis: verum