:: deftheorem defines Prob DIST_2:def 4 :
for S being non empty finite set
for D being EqSampleSpaces of S
for s being Element of D
for judgefunc being Function of S,BOOLEAN holds Prob (judgefunc,s) = (card (trueEVENT (judgefunc * s))) / (len s);