theorem :: CARDFIN2:18

for s, t being non empty finite set st card s = 23 & card t = 365 holds
prob (not-one-to-one (s,t)) > 1 / 2