theorem :: BOR_CANT:18

for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma st A is_all_independent_wrt Prob holds
( ( Prob . (lim_inf (Complement A)) = 0 or Prob . (lim_inf (Complement A)) = 1 ) & ( Prob . (lim_sup A) = 0 or Prob . (lim_sup A) = 1 ) )