theorem Th85: :: SETLIM_2:85

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)