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 \/ B) <= (P . A) + (P . B)
let Sigma be SigmaField of Omega; :: thesis: for A, B being Event of Sigma
for P being Probability of Sigma holds P . (A \/ B) <= (P . A) + (P . B)
let A, B be Event of Sigma; :: thesis: for P being Probability of Sigma holds P . (A \/ B) <= (P . A) + (P . B)
let P be Probability of Sigma; :: thesis: P . (A \/ B) <= (P . A) + (P . B)
A1: 0 <= P . (A /\ B) by Def13;
P . (A \/ B) = ((P . A) + (P . B)) - (P . (A /\ B)) by Th74;
hence P . (A \/ B) <= (P . A) + (P . B) by A1, XREAL_1:45; :: thesis: verum