for X being set
for Si being SigmaField of X
for S being SetSequence of Si holds lim_inf S = (lim_sup (Complement S)) `