theorem Th72: :: SETLIM_2:72

for X being set
for A1, A2 being SetSequence of X st A2 is convergent holds
lim_sup (A1 (\) A2) = (lim_sup A1) \ (lim_sup A2)