let A, B, C be SetSequence of the carrier of (TOP-REAL 2); :: thesis: ( ( for i being Nat holds C . i = (A . i) /\ (B . i) ) implies Lim_sup C c= (Lim_sup A) /\ (Lim_sup B) )
assume A1: for i being Nat holds C . i = (A . i) /\ (B . i) ; :: thesis: Lim_sup C c= (Lim_sup A) /\ (Lim_sup B)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lim_sup C or x in (Lim_sup A) /\ (Lim_sup B) )
assume x in Lim_sup C ; :: thesis: x in (Lim_sup A) /\ (Lim_sup B)
then consider C1 being subsequence of C such that
A2: x in Lim_inf C1 by Def2;
for i being Nat holds C . i c= B . i

proof

let i be Nat; :: thesis: C . i c= B . i
C . i = (A . i) /\ (B . i) by A1;
hence C . i c= B . i by XBOOLE_1:17; :: thesis: verum

end;

then consider E1 being subsequence of B such that
A3: for i being Nat holds C1 . i c= E1 . i by Th32;
Lim_inf C1 c= Lim_inf E1 by A3, Th17;
then A4: x in Lim_sup B by A2, Def2;
for i being Nat holds C . i c= A . i

proof

let i be Nat; :: thesis: C . i c= A . i
C . i = (A . i) /\ (B . i) by A1;
hence C . i c= A . i by XBOOLE_1:17; :: thesis: verum

end;

then consider D1 being subsequence of A such that
A5: for i being Nat holds C1 . i c= D1 . i by Th32;
Lim_inf C1 c= Lim_inf D1 by A5, Th17;
then x in Lim_sup A by A2, Def2;
hence x in (Lim_sup A) /\ (Lim_sup B) by A4, XBOOLE_0:def 4; :: thesis: verum