let E be non empty finite set ; :: thesis: for A being Event of E holds prob A <= 1
let A be Event of E; :: thesis: prob A <= 1
0 < card E by Lm1;
then (card A) * ((card E) ") <= (card E) * ((card E) ") by NAT_1:43, XREAL_1:64;
then (card A) / (card E) <= (card E) * ((card E) ") by XCMPLX_0:def 9;
then ( prob ([#] E) = (card E) / (card E) & prob A <= (card E) / (card E) ) by XCMPLX_0:def 9;
hence prob A <= 1 by XCMPLX_1:60; :: thesis: verum