:: deftheorem defines Probability DIST_2:def 8 :
for S being non empty finite set
for D being EqSampleSpaces of S
for b₃ being Function of (Funcs (S,BOOLEAN)),REAL holds
( b₃ is Probability of D iff for judgefunc being Element of Funcs (S,BOOLEAN) holds b₃ . judgefunc = Prob (judgefunc,D) );