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
( @lim_inf (Complement A) = (@lim_sup A) ` & (Prob . (@lim_inf (Complement A))) + (Prob . (@lim_sup A)) = 1 & (Prob . (lim_inf (Complement A))) + (Prob . (lim_sup A)) = 1 )