:: deftheorem defines Trivial-Probability DIST_2:def 9 :
for S being non empty finite set
for D being EqSampleSpaces of S
for b₃ being Probability of Trivial-SigmaField S holds
( b₃ = Trivial-Probability D iff for x being set st x in Trivial-SigmaField S holds
ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & b₃ . x = Prob (ch,D) ) );