theorem Th69: :: SETLIM_2:69

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