let n be Nat; :: thesis: for r being Point of (TOP-REAL n)
for X being Subset of (TOP-REAL n) st r in Cl X holds
ex seq being Real_Sequence of n st
( rng seq c= X & seq is convergent & lim seq = r )
let r be Point of (TOP-REAL n); :: thesis: for X being Subset of (TOP-REAL n) st r in Cl X holds
ex seq being Real_Sequence of n st
( rng seq c= X & seq is convergent & lim seq = r )
let X be Subset of (TOP-REAL n); :: thesis: ( r in Cl X implies ex seq being Real_Sequence of n st
( rng seq c= X & seq is convergent & lim seq = r ) )
reconsider r9 = r as Point of (Euclid n) by TOPREAL3:8;
defpred S₁[ object , object ] means ex z being Nat st
( $1 = z & $2 = the Element of X /\ (Ball (r9,(1 / (z + 1)))) );
assume A1: r in Cl X ; :: thesis: ex seq being Real_Sequence of n st
( rng seq c= X & seq is convergent & lim seq = r )

A2: now :: thesis: for x being object st x in NAT holds
ex u being object st
( u in the carrier of (TOP-REAL n) & S₁[x,u] )

let x be object ; :: thesis: ( x in NAT implies ex u being object st
( u in the carrier of (TOP-REAL n) & S₁[x,u] ) )
assume x in NAT ; :: thesis: ex u being object st
( u in the carrier of (TOP-REAL n) & S₁[x,u] )
then reconsider k = x as Nat ;
set n1 = k + 1;
set oi = Ball (r9,(1 / (k + 1)));
reconsider oi = Ball (r9,(1 / (k + 1))) as open Subset of (TOP-REAL n) by Th1;
reconsider u = the Element of X /\ oi as object ;
take u = u; :: thesis: ( u in the carrier of (TOP-REAL n) & S₁[x,u] )
dist (r9,r9) < 1 / (k + 1) by METRIC_1:1;
then r in oi by METRIC_1:11;
then X meets oi by A1, PRE_TOPC:24;
then not X /\ oi is empty ;
then u in X /\ oi ;
hence u in the carrier of (TOP-REAL n) ; :: thesis: S₁[x,u]
thus S₁[x,u] ; :: thesis: verum

end;

consider seq being Function such that
A3: ( dom seq = NAT & rng seq c= the carrier of (TOP-REAL n) ) and
A4: for x being object st x in NAT holds
S₁[x,seq . x] from FUNCT_1:sch 6(A2);
reconsider seq = seq as Real_Sequence of n by A3, FUNCT_2:def 1, RELSET_1:4;
take seq ; :: thesis: ( rng seq c= X & seq is convergent & lim seq = r )
thus rng seq c= X :: thesis: ( seq is convergent & lim seq = r )

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng seq or y in X )
assume y in rng seq ; :: thesis: y in X
then consider x being object such that
A5: x in dom seq and
A6: seq . x = y by FUNCT_1:def 3;
consider k being Nat such that
x = k and
A7: seq . x = the Element of X /\ (Ball (r9,(1 / (k + 1)))) by A4, A5;
set n1 = k + 1;
reconsider oi = Ball (r9,(1 / (k + 1))) as open Subset of (TOP-REAL n) by Th1;
dist (r9,r9) < 1 / (k + 1) by METRIC_1:1;
then r in oi by METRIC_1:11;
then X meets oi by A1, PRE_TOPC:24;
then not X /\ oi is empty ;
hence y in X by A6, A7, XBOOLE_0:def 4; :: thesis: verum

end;

A8: now :: thesis: for p being Real st 0 < p holds
ex k being Nat st
for m being Nat st k <= m holds
|.((seq . m) - r).| < p

let p be Real; :: thesis: ( 0 < p implies ex k being Nat st
for m being Nat st k <= m holds
|.((seq . m) - r).| < p )
set cp = [/(1 / p)\];
A9: 1 / p <= [/(1 / p)\] by INT_1:def 7;
assume A10: 0 < p ; :: thesis: ex k being Nat st
for m being Nat st k <= m holds
|.((seq . m) - r).| < p
then A11: 0 < [/(1 / p)\] by INT_1:def 7;
then reconsider cp = [/(1 / p)\] as Element of NAT by INT_1:3;
reconsider cp = cp as Nat ;
take k = cp; :: thesis: for m being Nat st k <= m holds
|.((seq . m) - r).| < p
k < k + 1 by NAT_1:13;
then A12: 1 / (k + 1) < 1 / k by A11, XREAL_1:88;
1 / (1 / p) >= 1 / cp by A10, A9, XREAL_1:85;
then A13: 1 / (k + 1) < p by A12, XXREAL_0:2;
let m be Nat; :: thesis: ( k <= m implies |.((seq . m) - r).| < p )
assume k <= m ; :: thesis: |.((seq . m) - r).| < p
then A14: k + 1 <= m + 1 by XREAL_1:6;
set m1 = m + 1;
1 / (m + 1) <= 1 / (k + 1) by A14, XREAL_1:85;
then A15: 1 / (m + 1) < p by A13, XXREAL_0:2;
set oi = Ball (r9,(1 / (m + 1)));
reconsider oi = Ball (r9,(1 / (m + 1))) as open Subset of (TOP-REAL n) by Th1;
dist (r9,r9) < 1 / (m + 1) by METRIC_1:1;
then r in oi by METRIC_1:11;
then X meets oi by A1, PRE_TOPC:24;
then A16: not X /\ oi is empty ;
m in NAT by ORDINAL1:def 12;
then ex m9 being Nat st
( m9 = m & seq . m = the Element of X /\ (Ball (r9,(1 / (m9 + 1)))) ) by A4;
then seq . m in oi by A16, XBOOLE_0:def 4;
hence |.((seq . m) - r).| < p by A15, Th2, XXREAL_0:2; :: thesis: verum

end;

hence seq is convergent by TOPRNS_1:def 8; :: thesis: lim seq = r
hence lim seq = r by A8, TOPRNS_1:def 9; :: thesis: verum