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
A1: prob ([#] E) = (card E) / (card E) ;
0 < card E by Lm1;
then 0 <= (card E) " ;
then (card A) * ((card E) " ) <= (card E) * ((card E) " ) by NAT_1:44, XREAL_1:66;
then (card A) / (card E) <= (card E) * ((card E) " ) by XCMPLX_0:def 9;
then prob A <= (card E) / (card E) by XCMPLX_0:def 9;
hence prob A <= 1 by A1, Th39; :: thesis: verum