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
A /\ B c= B by XBOOLE_1:17;
then (prob (A /\ B)) * ((prob B) ") <= (prob B) * ((prob B) ") by A1, Th19, XREAL_1:64;
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