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:
reconsider p9 = p as Point of (Euclid n) by TOPREAL3:8;
given s being Real_Sequence of n such that A1: s is convergent and
A2: for x being Nat holds s . x in S . x and
A3: p = lim s ; :: thesis:
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)

proof

let r be Real; :: thesis:
reconsider r9 = r as Real ;
assume r > 0 ; :: thesis:
then consider l being Nat such that
A4: for m being Nat st l <= m holds
|.((s . m) - p).| < r9 by A1, A3, TOPRNS_1:def 9;
reconsider v = max (0,l) as Nat by TARSKI:1;
take v ; :: thesis:
let m be Nat; :: thesis:
assume v < m ; :: thesis:
then l <= m by XXREAL_0:30;
then |.((s . m) - p).| < r9 by A4;
then A5: s . m in Ball (p9,r) by Th3;
s . m in S . m by A2;
hence S . m meets Ball (p9,r) by A5, XBOOLE_0:3; :: thesis:

end;

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