let E be non empty finite set ; :: thesis: for A, B being Event of E holds prob (A \ B) = (prob A) - (prob (A /\ B))
let A, B be Event of E; :: thesis: prob (A \ B) = (prob A) - (prob (A /\ B))
prob A = prob ((A \ B) \/ (A /\ B)) by XBOOLE_1:51;
then prob A = (prob (A \ B)) + (prob (A /\ B)) by Th47, XBOOLE_1:89;
hence prob (A \ B) = (prob A) - (prob (A /\ B)) ; :: thesis: verum