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 (card A) * ((card E) ") <= (card B) * ((card E) ") by A1, NAT_1:43, XREAL_1:64;
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