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 st 0 < P . B holds
(((P . A) + (P . B)) - 1) / (P . B) <= (P .|. B) . A
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for A, B being Event of Sigma st 0 < P . B holds
(((P . A) + (P . B)) - 1) / (P . B) <= (P .|. B) . A
let P be Probability of Sigma; :: thesis: for A, B being Event of Sigma st 0 < P . B holds
(((P . A) + (P . B)) - 1) / (P . B) <= (P .|. B) . A
let A, B be Event of Sigma; :: thesis: ( 0 < P . B implies (((P . A) + (P . B)) - 1) / (P . B) <= (P .|. B) . A )
assume A1: 0 < P . B ; :: thesis: (((P . A) + (P . B)) - 1) / (P . B) <= (P .|. B) . A
(((P . A) + (P . B)) - 1) / (P . B) <= (P . (A /\ B)) / (P . B) by A1, Th15, XREAL_1:72;
hence (((P . A) + (P . B)) - 1) / (P . B) <= (P .|. B) . A by A1, Def6; :: thesis: verum