let E be non empty finite set ; :: thesis: for A being Event of E holds 0 <= prob A
let A be Event of E; :: thesis: 0 <= prob A
0 < card E by Lm1;
then A1: 0 <= (card E) " ;
0 <= card A by CARD_1:47, NAT_1:44, XBOOLE_1:2;
then 0 * ((card E) " ) <= (card A) * ((card E) " ) by A1;
hence 0 <= prob A by XCMPLX_0:def 9; :: thesis: verum