let E be non empty finite set ; :: thesis: for A, B being Event of E holds (prob A) - (prob B) <= prob (A \ B)
let A, B be Event of E; :: thesis: (prob A) - (prob B) <= prob (A \ B)
prob (A /\ B) <= prob B by Th19, XBOOLE_1:17;
then (prob A) - (prob B) <= (prob A) - (prob (A /\ B)) by XREAL_1:13;
hence (prob A) - (prob B) <= prob (A \ B) by Th23; :: thesis: verum