theorem Th68: :: SETLIM_2:68

for X being set
for A1, A2 being SetSequence of X holds lim_sup (A1 (\/) A2) = (lim_sup A1) \/ (lim_sup A2)