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

let H be a_neighborhood of p; :: thesis:
consider H1 being non empty Subset of T such that
A3: H1 is a_neighborhood of p and
A4: H1 is open and
A5: H1 c= H by CONNSP_2:5;
consider k being Nat such that
A6: for m being Nat st m > k holds
G . m meets H1 by A2, A3, Def1;
take k ; :: thesis:
let m be Nat; :: thesis:
assume m > k ; :: thesis:
then G . m meets H1 by A6;
then consider y being object such that
A7: y in G . m and
A8: y in H1 by XBOOLE_0:3;
reconsider y = y as Point of T by A7;
H1 is a_neighborhood of y by A4, A8, CONNSP_2:3;
then consider H9 being non empty Subset of T such that
A9: H9 is a_neighborhood of y and
H9 is open and
A10: H9 c= H1 by CONNSP_2:5;
y in Cl (F . m) by A1, A7;
then H9 meets F . m by A9, CONNSP_2:27;
then H1 meets F . m by A10, XBOOLE_1:63;
hence F . m meets H by A5, XBOOLE_1:63; :: thesis:

end;

end;

let i be Nat; :: thesis:
G . i = Cl (F . i) by A1;
hence F . i c= G . i by PRE_TOPC:18; :: thesis:

end;