let E be non empty finite set ; :: thesis: for A, B being Event of E st 0 < prob B holds
prob A,B <= 1
let A, B be Event of E; :: thesis: ( 0 < prob B implies prob A,B <= 1 )
assume A1: 0 < prob B ; :: thesis: prob A,B <= 1
then A2: 0 <= (prob B) " ;
A /\ B c= B by XBOOLE_1:17;
then (prob (A /\ B)) * ((prob B) " ) <= (prob B) * ((prob B) " ) by A2, Th44, XREAL_1:66;
then (prob (A /\ B)) * ((prob B) " ) <= 1 by A1, XCMPLX_0:def 7;
hence prob A,B <= 1 by XCMPLX_0:def 9; :: thesis: verum