let E be non empty finite set ; :: thesis: for A, B being Event of E holds prob A = (prob (A \/ B)) - (prob (B \ A))
let A, B be Event of E; :: thesis: prob A = (prob (A \/ B)) - (prob (B \ A))
prob (A \/ (B \ A)) = prob (A \/ B) by XBOOLE_1:39;
then prob (A \/ B) = (prob A) + (prob (B \ A)) by Th21, XBOOLE_1:79;
hence prob A = (prob (A \/ B)) - (prob (B \ A)) ; :: thesis: verum