theorem Th16: :: BOR_CANT:16

for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma holds
( ( Partial_Sums (Prob * A) is convergent implies ( Prob . (lim_sup A) = 0 & Prob . (lim_inf (Complement A)) = 1 ) ) & ( A is_all_independent_wrt Prob & Partial_Sums (Prob * A) is divergent_to+infty implies ( Prob . (lim_inf (Complement A)) = 0 & Prob . (lim_sup A) = 1 ) ) )