let E be non empty finite set ; :: thesis: for A, B being Event of E holds prob (A \/ B) <= (prob A) + (prob B)
let A, B be Event of E; :: thesis: prob (A \/ B) <= (prob A) + (prob B)
prob (A \/ B) = ((prob A) + (prob B)) - (prob (A /\ B)) by Th20;
hence prob (A \/ B) <= (prob A) + (prob B) by Th18, XREAL_1:43; :: thesis: verum