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 Th48;
(prob B) - 1 < 1 - 1 by A2, XREAL_1:11;
then 0 < - (- (1 - (prob B))) ;
then prob (A ` ),(B ` ) = 1 - (prob A,(B ` )) by A4, Th70;
hence prob (A ` ),(B ` ) = 1 - ((prob A) / (1 - (prob B))) by A1, A2, A3, Th76; :: thesis: verum