let E be non empty finite set ; :: thesis: for A, B being Event of E st B c= A holds
prob (A \ B) = (prob A) - (prob B)
let A, B be Event of E; :: thesis: ( B c= A implies prob (A \ B) = (prob A) - (prob B) )
assume B c= A ; :: thesis: prob (A \ B) = (prob A) - (prob B)
then prob (A /\ B) = prob B by XBOOLE_1:28;
hence prob (A \ B) = (prob A) - (prob B) by Th23; :: thesis: verum