let E be non empty finite set ; :: thesis: for A, B being Event of E st 0 < prob B holds
0 <= prob (A,B)
let A, B be Event of E; :: thesis: ( 0 < prob B implies 0 <= prob (A,B) )
assume A1: 0 < prob B ; :: thesis: 0 <= prob (A,B)
0 <= prob (A /\ B) by Th18;
hence 0 <= prob (A,B) by A1; :: thesis: verum