let s, t be non empty finite set ; :: thesis: ( card s = 23 & card t = 365 implies prob (not-one-to-one s,t) > 1 / 2 )
assume Z0: card s = 23 ; :: thesis: ( not card t = 365 or prob (not-one-to-one s,t) > 1 / 2 )
assume Z1: card t = 365 ; :: thesis: prob (not-one-to-one s,t) > 1 / 2
set E = not-one-to-one s,t;
set comega = card (Funcs s,t);
(2 * (card (not-one-to-one s,t))) / 2 > (card (Funcs s,t)) / 2 by XREAL_1:76, Th9, Z0, Z1;
then (card (not-one-to-one s,t)) / (card (Funcs s,t)) > ((card (Funcs s,t)) / 2) / (card (Funcs s,t)) by XREAL_1:76;
then (card (not-one-to-one s,t)) / (card (Funcs s,t)) > ((card (Funcs s,t)) / (card (Funcs s,t))) / 2 ;
then (card (not-one-to-one s,t)) / (card (Funcs s,t)) > 1 / 2 by XCMPLX_0:def 7;
hence prob (not-one-to-one s,t) > 1 / 2 by RPR_1:def 4; :: thesis: verum