:: deftheorem Def8 defines Probability PROB_1:def 8 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for b₃ being Function of Sigma,REAL holds
( b₃ is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= b₃ . A ) & b₃ . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
b₃ . (A \/ B) = (b₃ . A) + (b₃ . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
( b₃ * ASeq is convergent & lim (b₃ * ASeq) = b₃ . (Intersection ASeq) ) ) ) );