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 set ; :: 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

let G be a_neighborhood of x9; :: thesis: ex k being Element of NAT st
for m being Element of 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 set 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 Element of NAT such that
A4: for m being Element of NAT st m > k holds
S . m meets Int G by A2, Def11;
take k = k; :: thesis: for m being Element of NAT st m > k holds
S . m meets G
let m be Element of 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 Def11; :: thesis: verum

end;

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