theorem :: RPR_1:14

for E being non empty finite set
for e being Singleton of E holds prob e = 1 / (card E) by CARD_1:def 7;