let E be non empty finite set ; :: thesis: for A, B being Event of E st 0 < prob B holds
prob (A,B) = 1 - ((prob (B \ A)) / (prob B))
let A, B be Event of E; :: thesis: ( 0 < prob B implies prob (A,B) = 1 - ((prob (B \ A)) / (prob B)) )
(prob (B \ A)) + (prob (A /\ B)) = ((prob B) - (prob (A /\ B))) + (prob (A /\ B)) by Th23;
then prob (A,B) = ((prob B) - (prob (B \ A))) / (prob B) ;
then A1: prob (A,B) = ((prob B) / (prob B)) - ((prob (B \ A)) / (prob B)) by XCMPLX_1:120;
assume 0 < prob B ; :: thesis: prob (A,B) = 1 - ((prob (B \ A)) / (prob B))
hence prob (A,B) = 1 - ((prob (B \ A)) / (prob B)) by A1, XCMPLX_1:60; :: thesis: verum