let n be Nat; :: thesis:
let S be SetSequence of the carrier of (TOP-REAL n); :: thesis:
let p be Point of (TOP-REAL n); :: thesis:
let p9 be Point of (Euclid n); :: thesis:
assume A1: p = p9 ; :: thesis:

hereby :: thesis:

assume A2: p in Lim_inf S ; :: thesis:
let r be Real; :: thesis:
assume r > 0 ; :: thesis:
then reconsider G = Ball (p9,r) as a_neighborhood of p by A1, GOBOARD6:2;
ex k being Nat st
for m being Nat st m > k holds
S . m meets G by A2, Def1;
hence ex k being Nat st
for m being Nat st m > k holds
S . m meets Ball (p9,r) ; :: thesis:

end;

assume A3: for r being Real st r > 0 holds
ex k being Nat st
for m being Nat st m > k holds
S . m meets Ball (p9,r) ; :: thesis:

now :: thesis:

let G be a_neighborhood of p; :: thesis:
A4: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider G9 = Int G as Subset of (TopSpaceMetr (Euclid n)) ;
A5: p9 in G9 by A1, CONNSP_2:def 1;
G9 is open by A4, PRE_TOPC:30;
then consider r being Real such that
A6: r > 0 and
A7: Ball (p9,r) c= G9 by A5, TOPMETR:15;
consider k being Nat such that
A8: for m being Nat st m > k holds
S . m meets Ball (p9,r) by A3, A6;
take k = k; :: thesis:
let m be Nat; :: thesis:
assume m > k ; :: thesis:
then ( G9 c= G & S . m meets Ball (p9,r) ) by A8, TOPS_1:16;
hence S . m meets G by A7, XBOOLE_1:1, XBOOLE_1:63; :: thesis:

end;

hence p in Lim_inf S by Def1; :: thesis: