let F, G be SetSequence of the carrier of (TOP-REAL 2); :: thesis: ( ( for i being Nat holds G . i = Cl (F . i) ) implies Lim_sup G = Lim_sup F )
assume A1: for i being Nat holds G . i = Cl (F . i) ; :: thesis: Lim_sup G = Lim_sup F
thus Lim_sup G c= Lim_sup F :: according to XBOOLE_0:def 10 :: thesis: Lim_sup F c= Lim_sup G

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lim_sup G or x in Lim_sup F )
assume x in Lim_sup G ; :: thesis: x in Lim_sup F
then consider H being subsequence of G such that
A2: x in Lim_inf H by Def2;
consider NS being increasing sequence of NAT such that
A3: H = G * NS by VALUED_0:def 17;
set P = F * NS;
reconsider P = F * NS as SetSequence of (TOP-REAL 2) ;
reconsider P = P as subsequence of F ;
for i being Nat holds H . i = Cl (P . i)

proof

let i be Nat; :: thesis: H . i = Cl (P . i)
A4: i in NAT by ORDINAL1:def 12;
A5: dom NS = NAT by FUNCT_2:def 1;
then H . i = G . (NS . i) by A3, FUNCT_1:13, A4
.= Cl (F . (NS . i)) by A1
.= Cl (P . i) by A5, FUNCT_1:13, A4 ;
hence H . i = Cl (P . i) ; :: thesis: verum

end;

then Lim_inf H = Lim_inf P by Th20;
hence x in Lim_sup F by A2, Def2; :: thesis: verum

end;

for i being Nat holds F . i c= G . i

proof

let i be Nat; :: thesis: F . i c= G . i
G . i = Cl (F . i) by A1;
hence F . i c= G . i by PRE_TOPC:18; :: thesis: verum

end;

hence Lim_sup F c= Lim_sup G by Th34; :: thesis: verum