let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being Event of Sigma holds P . (A \ B) = (P . (A \/ B)) - (P . B)

let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for A, B being Event of Sigma holds P . (A \ B) = (P . (A \/ B)) - (P . B)

let P be Probability of Sigma; :: thesis: for A, B being Event of Sigma holds P . (A \ B) = (P . (A \/ B)) - (P . B)
let A, B be Event of Sigma; :: thesis: P . (A \ B) = (P . (A \/ B)) - (P . B)
(P . (A \/ B)) - (P . B) = ((P . B) + (P . (A \ B))) - (P . B) by PROB_1:36;
hence P . (A \ B) = (P . (A \/ B)) - (P . B) ; :: thesis: verum