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