let s, t be non empty finite set ; ( card s = 23 & card t = 365 implies prob (not-one-to-one (s,t)) > 1 / 2 )
assume A1:
card s = 23
; ( not card t = 365 or prob (not-one-to-one (s,t)) > 1 / 2 )
assume A2:
card t = 365
; 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 Th17, A1, A2, XREAL_1:74;
then
(card (not-one-to-one (s,t))) / (card (Funcs (s,t))) > ((card (Funcs (s,t))) / 2) / (card (Funcs (s,t)))
by XREAL_1:74;
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 1; verum