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

let G be a_neighborhood of x9; :: thesis:
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:
let m be Nat; :: thesis:
assume m > k ; :: thesis:
then S . m meets Int G by A4;
hence S . m meets G by TOPS_1:16, XBOOLE_1:63; :: thesis:

end;

end;