theorem Th83: :: SETLIM_2:83

for X being set
for A being Subset of X
for A1 being SetSequence of X holds A \ (lim_sup A1) c= lim_sup (A (\) A1)