let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma st 0 < P . B holds
1 - ((P . (([#] Sigma) \ A)) / (P . B)) <= (P .|. B) . A
let Sigma be SigmaField of Omega; :: thesis: for A, B being Event of Sigma
for P being Probability of Sigma st 0 < P . B holds
1 - ((P . (([#] Sigma) \ A)) / (P . B)) <= (P .|. B) . A
let A, B be Event of Sigma; :: thesis: for P being Probability of Sigma st 0 < P . B holds
1 - ((P . (([#] Sigma) \ A)) / (P . B)) <= (P .|. B) . A
let P be Probability of Sigma; :: thesis: ( 0 < P . B implies 1 - ((P . (([#] Sigma) \ A)) / (P . B)) <= (P .|. B) . A )
assume A1: 0 < P . B ; :: thesis: 1 - ((P . (([#] Sigma) \ A)) / (P . B)) <= (P .|. B) . A
((P . B) + (P . A)) - 1 <= P . (A /\ B) by Th15;
then (P . B) + (- (1 - (P . A))) <= P . (A /\ B) ;
then (P . B) + (- (P . (([#] Sigma) \ A))) <= P . (A /\ B) by PROB_1:32;
then ((P . B) + (- (P . (([#] Sigma) \ A)))) / (P . B) <= (P . (A /\ B)) / (P . B) by A1, XREAL_1:72;
then ((P . B) - (P . (([#] Sigma) \ A))) / (P . B) <= (P .|. B) . A by A1, Def6;
then ((P . B) / (P . B)) - ((P . (([#] Sigma) \ A)) / (P . B)) <= (P .|. B) . A by XCMPLX_1:120;
hence 1 - ((P . (([#] Sigma) \ A)) / (P . B)) <= (P .|. B) . A by A1, XCMPLX_1:60; :: thesis: verum