let T be non empty TopSpace; :: thesis: for F, G being SetSequence of the carrier of T st ( for i being Nat holds G . i = Cl (F . i) ) holds
Lim_inf G = Lim_inf F
let F, G be SetSequence of the carrier of T; :: thesis: ( ( for i being Nat holds G . i = Cl (F . i) ) implies Lim_inf G = Lim_inf F )
assume A1: for i being Nat holds G . i = Cl (F . i) ; :: thesis: Lim_inf G = Lim_inf F
thus Lim_inf G c= Lim_inf F :: according to XBOOLE_0:def 10 :: thesis: Lim_inf F c= Lim_inf G

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lim_inf G or x in Lim_inf F )
assume A2: x in Lim_inf G ; :: thesis: x in Lim_inf F
then reconsider p = x as Point of T ;
for H being a_neighborhood of p ex k being Nat st
for m being Nat st m > k holds
F . m meets H

proof

let H be a_neighborhood of p; :: thesis: ex k being Nat st
for m being Nat st m > k holds
F . m meets H
consider H1 being non empty Subset of T such that
A3: H1 is a_neighborhood of p and
A4: H1 is open and
A5: H1 c= H by CONNSP_2:5;
consider k being Nat such that
A6: for m being Nat st m > k holds
G . m meets H1 by A2, A3, Def1;
take k ; :: thesis: for m being Nat st m > k holds
F . m meets H
let m be Nat; :: thesis: ( m > k implies F . m meets H )
assume m > k ; :: thesis: F . m meets H
then G . m meets H1 by A6;
then consider y being object such that
A7: y in G . m and
A8: y in H1 by XBOOLE_0:3;
reconsider y = y as Point of T by A7;
H1 is a_neighborhood of y by A4, A8, CONNSP_2:3;
then consider H9 being non empty Subset of T such that
A9: H9 is a_neighborhood of y and
H9 is open and
A10: H9 c= H1 by CONNSP_2:5;
y in Cl (F . m) by A1, A7;
then H9 meets F . m by A9, CONNSP_2:27;
then H1 meets F . m by A10, XBOOLE_1:63;
hence F . m meets H by A5, XBOOLE_1:63; :: thesis: verum

end;

hence x in Lim_inf F by Def1; :: 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_inf F c= Lim_inf G by Th17; :: thesis: verum