:: deftheorem Def1 defines Trivial-Probability RANDOM_1:def 1 :
for E being non empty finite set
for b₂ being Probability of Trivial-SigmaField E holds
( b₂ = Trivial-Probability E iff for A being Event of E holds b₂ . A = prob A );