let E be non empty finite set ; :: thesis: for A, B being Event of E st A c= B holds
prob A <= prob B
let A, B be Event of E; :: thesis: ( A c= B implies prob A <= prob B )
assume A1: A c= B ; :: thesis: prob A <= prob B
0 < card E by Lm1;
then 0 <= (card E) " ;
then (card A) * ((card E) " ) <= (card B) * ((card E) " ) by A1, NAT_1:44, XREAL_1:66;
then (card A) / (card E) <= (card B) * ((card E) " ) by XCMPLX_0:def 9;
hence prob A <= prob B by XCMPLX_0:def 9; :: thesis: verum