let F, G be SetSequence of the carrier of (TOP-REAL 2); :: thesis: ( ( for i being Element of NAT holds G . i = Cl (F . i) ) implies Lim_sup G = Lim_sup F )
assume A1: for i being Element of NAT holds G . i = Cl (F . i) ; :: thesis: Lim_sup G = Lim_sup F
A2: for i being Element of NAT holds F . i c= G . i

proof

let i be Element of NAT ; :: thesis: F . i c= G . i
G . i = Cl (F . i) by A1;
hence F . i c= G . i by PRE_TOPC:48; :: thesis: verum

end;

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 set ; :: 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
A3: x in Lim_inf H by Def12;
consider NS being increasing sequence of NAT such that
A4: 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 Element of NAT holds H . i = Cl (P . i)

proof

let i be Element of NAT ; :: thesis: H . i = Cl (P . i)
A5: dom NS = NAT by FUNCT_2:def 1;
then H . i = G . (NS . i) by A4, FUNCT_1:23
.= Cl (F . (NS . i)) by A1
.= Cl (P . i) by A5, FUNCT_1:23 ;
hence H . i = Cl (P . i) ; :: thesis: verum

end;

then Lim_inf H = Lim_inf P by Th57;
hence x in Lim_sup F by A3, Def12; :: thesis: verum

end;

thus Lim_sup F c= Lim_sup G by A2, Th71; :: thesis: verum