theorem :: KURATO_0:13

for X being set
for A, B, C being SetSequence of X st ( for n being Nat holds C . n = (A . n) /\ (B . n) ) holds
lim_sup C c= (lim_sup A) /\ (lim_sup B)