let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for A being Event of Sigma
for P being Probability of Sigma holds P . A = 1 - (P . (([#] Sigma) \ A))
let Sigma be SigmaField of Omega; :: thesis: for A being Event of Sigma
for P being Probability of Sigma holds P . A = 1 - (P . (([#] Sigma) \ A))
let A be Event of Sigma; :: thesis: for P being Probability of Sigma holds P . A = 1 - (P . (([#] Sigma) \ A))
let P be Probability of Sigma; :: thesis: P . A = 1 - (P . (([#] Sigma) \ A))
(P . (([#] Sigma) \ A)) + (P . A) = 1 by PROB_1:31;
hence P . A = 1 - (P . (([#] Sigma) \ A)) ; :: thesis: verum