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 . (([#] Sigma) \ A) = 1 - (P . A)

let Sigma be SigmaField of Omega; :: thesis: for A being Event of Sigma

for P being Probability of Sigma holds P . (([#] Sigma) \ A) = 1 - (P . A)

let A be Event of Sigma; :: thesis: for P being Probability of Sigma holds P . (([#] Sigma) \ A) = 1 - (P . A)

let P be Probability of Sigma; :: thesis: P . (([#] Sigma) \ A) = 1 - (P . A)

(P . (([#] Sigma) \ A)) + (P . A) = 1 by Th31;

hence P . (([#] Sigma) \ A) = 1 - (P . A) ; :: thesis: verum

for A being Event of Sigma

for P being Probability of Sigma holds P . (([#] Sigma) \ A) = 1 - (P . A)

let Sigma be SigmaField of Omega; :: thesis: for A being Event of Sigma

for P being Probability of Sigma holds P . (([#] Sigma) \ A) = 1 - (P . A)

let A be Event of Sigma; :: thesis: for P being Probability of Sigma holds P . (([#] Sigma) \ A) = 1 - (P . A)

let P be Probability of Sigma; :: thesis: P . (([#] Sigma) \ A) = 1 - (P . A)

(P . (([#] Sigma) \ A)) + (P . A) = 1 by Th31;

hence P . (([#] Sigma) \ A) = 1 - (P . A) ; :: thesis: verum