theorem :: SETLIM_1:57

for X being set
for B being SetSequence of X holds lim_sup B = (lim_inf (Complement B)) `