let T be non empty TopSpace; :: thesis: for F, G being SetSequence of the carrier of T st ( for i being Element of 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 Element of NAT holds G . i = Cl (F . i) ) implies Lim_inf G = Lim_inf F )
assume A1: for i being Element of 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 set ; :: 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 Element of NAT st
for m being Element of NAT st m > k holds
F . m meets H

proof

let H be a_neighborhood of p; :: thesis: ex k being Element of NAT st
for m being Element of 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 & H1 is open & H1 c= H ) by CONNSP_2:7;
consider k being Element of NAT such that
A4: for m being Element of NAT st m > k holds
G . m meets H1 by A2, A3, Def11;
take k ; :: thesis: for m being Element of NAT st m > k holds
F . m meets H
let m be Element of NAT ; :: thesis: ( m > k implies F . m meets H )
assume m > k ; :: thesis: F . m meets H
then G . m meets H1 by A4;
then consider y being set such that
A5: ( y in G . m & y in H1 ) by XBOOLE_0:3;
reconsider y = y as Point of T by A5;
H1 is a_neighborhood of y by A3, A5, CONNSP_2:5;
then consider H' being non empty Subset of T such that
A6: ( H' is a_neighborhood of y & H' is open & H' c= H1 ) by CONNSP_2:7;
y in Cl (F . m) by A1, A5;
then H' meets F . m by A6, CONNSP_2:34;
then H1 meets F . m by A6, XBOOLE_1:63;
hence F . m meets H by A3, XBOOLE_1:63; :: thesis: verum

end;

hence x in Lim_inf F by Def11; :: thesis: verum

end;

thus Lim_inf F c= Lim_inf G :: thesis: verum

proof

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;

hence Lim_inf F c= Lim_inf G by Th54; :: thesis: verum

end;