:: deftheorem defines prob RPR_1:def 1 :
for E being finite set
for A being Event of E holds prob A = (card A) / (card E);