theorem :: KURATO_2:35

for A, B, C being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Nat holds C . i = (A . i) \/ (B . i) ) holds
(Lim_sup A) \/ (Lim_sup B) c= Lim_sup C