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 & 0 <= card A ) by Lm1, CARD_1:27;
hence 0 <= prob A ; :: thesis: verum