let E be non empty finite set ; :: thesis: for A, B being Event of E st 0 < prob A & prob B < 1 & A misses B holds
prob ((A `),(B `)) = 1 - ((prob A) / (1 - (prob B)))
let A, B be Event of E; :: thesis: ( 0 < prob A & prob B < 1 & A misses B implies prob ((A `),(B `)) = 1 - ((prob A) / (1 - (prob B))) )
assume that
A1: 0 < prob A and
A2: prob B < 1 and
A3: A misses B ; :: thesis: prob ((A `),(B `)) = 1 - ((prob A) / (1 - (prob B)))
A4: prob (B `) = 1 - (prob B) by Th22;
(prob B) - 1 < 1 - 1 by A2, XREAL_1:9;
then 0 < - (- (1 - (prob B))) ;
then prob ((A `),(B `)) = 1 - (prob (A,(B `))) by A4, Th40;
hence prob ((A `),(B `)) = 1 - ((prob A) / (1 - (prob B))) by A1, A2, A3, Th46; :: thesis: verum