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

proof

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

proof

let G be a_neighborhood of p; :: thesis: ex k being Nat st
for m being Nat st m > k holds
F . m meets G
take k = 1; :: thesis: for m being Nat st m > k holds
F . m meets G
let m be Nat; :: thesis: ( m > k implies F . m meets G )
assume m > k ; :: thesis: F . m meets G
F . m = A by A1;
hence F . m meets G by A2, CONNSP_2:27; :: thesis: verum

end;

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

end;