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