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 holds ((P . A) + (P . B)) - 1 <= P . (A /\ B)

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

for P being Probability of Sigma holds ((P . A) + (P . B)) - 1 <= P . (A /\ B)

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

let P be Probability of Sigma; :: thesis: ((P . A) + (P . B)) - 1 <= P . (A /\ B)

((P . A) + (P . B)) - (P . (A /\ B)) = P . (A \/ B) by PROB_1:38;

then ((P . A) + (P . B)) - (P . (A /\ B)) <= 1 by PROB_1:35;

then (P . A) + (P . B) <= (P . (A /\ B)) + 1 by XREAL_1:20;

hence ((P . A) + (P . B)) - 1 <= P . (A /\ B) by XREAL_1:20; :: thesis: verum

for A, B being Event of Sigma

for P being Probability of Sigma holds ((P . A) + (P . B)) - 1 <= P . (A /\ B)

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

for P being Probability of Sigma holds ((P . A) + (P . B)) - 1 <= P . (A /\ B)

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

let P be Probability of Sigma; :: thesis: ((P . A) + (P . B)) - 1 <= P . (A /\ B)

((P . A) + (P . B)) - (P . (A /\ B)) = P . (A \/ B) by PROB_1:38;

then ((P . A) + (P . B)) - (P . (A /\ B)) <= 1 by PROB_1:35;

then (P . A) + (P . B) <= (P . (A /\ B)) + 1 by XREAL_1:20;

hence ((P . A) + (P . B)) - 1 <= P . (A /\ B) by XREAL_1:20; :: thesis: verum