:: deftheorem Def6 defines Prob DIST_2:def 6 :
for S being non empty finite set
for D being EqSampleSpaces of S
for judgefunc being Function of S,BOOLEAN
for b₄ being Real holds
( b₄ = Prob (judgefunc,D) iff for s being Element of D holds b₄ = Prob (judgefunc,s) );