let n be Element of 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 ) )
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 )
reconsider r' = r as Point of (Euclid n) by TOPREAL3:13;
defpred S₁[ set , set ] means ex z being Element of NAT st
( $1 = z & $2 = choose (X /\ (Ball r',(1 / (z + 1)))) );

A2: now

let x be set ; :: thesis: ( x in NAT implies ex u being set st
( u in the carrier of (TOP-REAL n) & S₁[x,u] ) )
assume x in NAT ; :: thesis: ex u being set st
( u in the carrier of (TOP-REAL n) & S₁[x,u] )
then reconsider k = x as Element of NAT ;
set n1 = k + 1;
set oi = Ball r',(1 / (k + 1));
reconsider oi = Ball r',(1 / (k + 1)) as open Subset of (TOP-REAL n) by Th30;
reconsider u = choose (X /\ oi) as set ;
take u = u; :: thesis: ( u in the carrier of (TOP-REAL n) & S₁[x,u] )
dist r',r' < 1 / (k + 1) by METRIC_1:1;
then r in oi by METRIC_1:12;
then X meets oi by A1, PRE_TOPC:54;
then not X /\ oi is empty by XBOOLE_0:def 7;
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 and
A4: rng seq c= the carrier of (TOP-REAL n) and
A5: for x being set st x in NAT holds
S₁[x,seq . x] from WELLORD2:sch 1(A2);
reconsider seq = seq as Real_Sequence of n by A3, A4, FUNCT_2:def 1, RELSET_1:11;
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 set ; :: 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 set such that
A6: ( x in dom seq & seq . x = y ) by FUNCT_1:def 5;
consider k being Element of NAT such that
A7: ( x = k & seq . x = choose (X /\ (Ball r',(1 / (k + 1)))) ) by A5, A6;
set n1 = k + 1;
reconsider oi = Ball r',(1 / (k + 1)) as open Subset of (TOP-REAL n) by Th30;
dist r',r' < 1 / (k + 1) by METRIC_1:1;
then r in oi by METRIC_1:12;
then X meets oi by A1, PRE_TOPC:54;
then not X /\ oi is empty by XBOOLE_0:def 7;
hence y in X by A6, A7, XBOOLE_0:def 4; :: thesis: verum

end;

A8: now

let p be Real; :: thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((seq . m) - r).| < p )
assume A9: 0 < p ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((seq . m) - r).| < p
set cp = [/(1 / p)\];
A11: 1 / p <= [/(1 / p)\] by INT_1:def 5;
A12: 0 < [/(1 / p)\] by A9, INT_1:def 5;
then reconsider cp = [/(1 / p)\] as Element of NAT by INT_1:16;
take k = cp; :: thesis: for m being Element of NAT st k <= m holds
|.((seq . m) - r).| < p
let m be Element of NAT ; :: thesis: ( k <= m implies |.((seq . m) - r).| < p )
assume A13: k <= m ; :: thesis: |.((seq . m) - r).| < p
consider m' being Element of NAT such that
A14: ( m' = m & seq . m = choose (X /\ (Ball r',(1 / (m' + 1)))) ) by A5;
set m1 = m + 1;
set oi = Ball r',(1 / (m + 1));
reconsider oi = Ball r',(1 / (m + 1)) as open Subset of (TOP-REAL n) by Th30;
dist r',r' < 1 / (m + 1) by METRIC_1:1;
then r in oi by METRIC_1:12;
then X meets oi by A1, PRE_TOPC:54;
then not X /\ oi is empty by XBOOLE_0:def 7;
then A15: seq . m in oi by A14, XBOOLE_0:def 4;
k + 1 <= m + 1 by A13, XREAL_1:8;
then A16: 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:87;
k < k + 1 by NAT_1:13;
then A17: 1 / (k + 1) < 1 / k by A12, XREAL_1:90;
1 / (1 / p) >= 1 / cp by A9, A11, XREAL_1:87;
then 1 / (k + 1) < p by A17, XXREAL_0:2;
then 1 / (m + 1) < p by A16, XXREAL_0:2;
hence |.((seq . m) - r).| < p by A15, Th32, XXREAL_0:2; :: thesis: verum

end;

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