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 ) )
reconsider r9 = 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 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

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 r9,(1 / (k + 1));
reconsider oi = Ball r9,(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 r9,r9 < 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 & rng seq c= the carrier of (TOP-REAL n) ) and
A4: 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, 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
A5: x in dom seq and
A6: seq . x = y by FUNCT_1:def 5;
consider k being Element of NAT such that
x = k and
A7: seq . x = choose (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 Th30;
dist r9,r9 < 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 )
set cp = [/(1 / p)\];
A9: 1 / p <= [/(1 / p)\] by INT_1:def 5;
assume A10: 0 < p ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((seq . m) - r).| < p
then A11: 0 < [/(1 / p)\] by 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
k < k + 1 by NAT_1:13;
then A12: 1 / (k + 1) < 1 / k by A11, XREAL_1:90;
1 / (1 / p) >= 1 / cp by A10, A9, XREAL_1:87;
then A13: 1 / (k + 1) < p by A12, XXREAL_0:2;
let m be Element of 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:8;
set m1 = m + 1;
1 / (m + 1) <= 1 / (k + 1) by A14, XREAL_1:87;
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 Th30;
dist r9,r9 < 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 A16: not X /\ oi is empty by XBOOLE_0:def 7;
ex m9 being Element of NAT st
( m9 = m & seq . m = choose (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, 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