let T be non empty TopSpace; :: thesis: for S being SetSequence of the carrier of T holds Cl (Lim_inf S) = Lim_inf S
let S be SetSequence of the carrier of T; :: thesis: Cl (Lim_inf S) = Lim_inf S
thus Cl (Lim_inf S) c= Lim_inf S :: according to XBOOLE_0:def 10 :: thesis: Lim_inf S c= Cl (Lim_inf S)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl (Lim_inf S) or x in Lim_inf S )
assume A1: x in Cl (Lim_inf S) ; :: thesis: x in Lim_inf S
then reconsider x9 = x as Point of T ;

now :: thesis: for G being a_neighborhood of x9 ex k being Nat st
for m being Nat st m > k holds
S . m meets G

let G be a_neighborhood of x9; :: thesis: ex k being Nat st
for m being Nat st m > k holds
S . m meets G
set H = Int G;
x9 in Int G by CONNSP_2:def 1;
then Lim_inf S meets Int G by A1, PRE_TOPC:24;
then consider z being object such that
A2: z in Lim_inf S and
A3: z in Int G by XBOOLE_0:3;
reconsider z = z as Point of T by A2;
z in Int (Int G) by A3;
then Int G is a_neighborhood of z by CONNSP_2:def 1;
then consider k being Nat such that
A4: for m being Nat st m > k holds
S . m meets Int G by A2, Def1;
take k = k; :: thesis: for m being Nat st m > k holds
S . m meets G
let m be Nat; :: thesis: ( m > k implies S . m meets G )
assume m > k ; :: thesis: S . m meets G
then S . m meets Int G by A4;
hence S . m meets G by TOPS_1:16, XBOOLE_1:63; :: thesis: verum

end;

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

end;

thus Lim_inf S c= Cl (Lim_inf S) by PRE_TOPC:18; :: thesis: verum