let n be Element of NAT ; :: thesis: for S being SetSequence of the carrier of (TOP-REAL n)
for p being Point of
for p' being Point of st p = p' holds
( p in Lim_inf S iff for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball p',r )
let S be SetSequence of the carrier of (TOP-REAL n); :: thesis: for p being Point of
for p' being Point of st p = p' holds
( p in Lim_inf S iff for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball p',r )
let p be Point of ; :: thesis: for p' being Point of st p = p' holds
( p in Lim_inf S iff for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball p',r )
let p' be Point of ; :: thesis: ( p = p' implies ( p in Lim_inf S iff for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball p',r ) )
assume A1: p = p' ; :: thesis: ( p in Lim_inf S iff for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball p',r )

hereby :: thesis: ( ( for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball p',r ) implies p in Lim_inf S )

assume A2: p in Lim_inf S ; :: thesis: for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball p',r
let r be real number ; :: thesis: ( r > 0 implies ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball p',r )
assume r > 0 ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball p',r
then reconsider G = Ball p',r as a_neighborhood of p by A1, GOBOARD6:5;
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G by A2, Def11;
hence ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball p',r ; :: thesis: verum

end;

assume A3: for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets Ball p',r ; :: thesis: p in Lim_inf S

now

let G be a_neighborhood of p; :: thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
S . m meets G
A4: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider G' = Int G as Subset of ;
A5: p' in G' by A1, CONNSP_2:def 1;
G' is open by A4, PRE_TOPC:60;
then consider r being real number such that
A6: r > 0 and
A7: Ball p',r c= G' by A5, TOPMETR:22;
consider k being Element of NAT such that
A8: for m being Element of NAT st m > k holds
S . m meets Ball p',r by A3, A6;
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 ( G' c= G & S . m meets Ball p',r ) by A8, TOPS_1:44;
hence S . m meets G by A7, XBOOLE_1:1, XBOOLE_1:63; :: thesis: verum

end;

hence p in Lim_inf S by Def11; :: thesis: verum