let X be Subset of REAL ; :: thesis: for r3 being Real st r3 in Cl X holds
ex seq being Real_Sequence st
( rng seq c= X & seq is convergent & lim seq = r3 )
let r3 be Real; :: thesis: ( r3 in Cl X implies ex seq being Real_Sequence st
( rng seq c= X & seq is convergent & lim seq = r3 ) )
assume A1: r3 in Cl X ; :: thesis: ex seq being Real_Sequence st
( rng seq c= X & seq is convergent & lim seq = r3 )
defpred S₁[ set , set ] means ex n being Nat st
( $1 = n & $2 = choose (X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[) );

A2: now

let x be set ; :: thesis: ( x in NAT implies ex u being set st
( u in REAL & S₁[x,u] ) )
assume x in NAT ; :: thesis: ex u being set st
( u in REAL & S₁[x,u] )
then reconsider n = x as Element of NAT ;
set n1 = n + 1;
set oi = ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[;
reconsider u = choose (X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[) as set ;
take u = u; :: thesis: ( u in REAL & S₁[x,u] )
A3: r3 < r3 + (1 / (n + 1)) by XREAL_1:31;
then r3 - (1 / (n + 1)) < r3 by XREAL_1:21;
then r3 in ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[ by A3;
then not X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[ is empty by A1, Th38;
then u in X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[ ;
hence u in REAL ; :: thesis: S₁[x,u]
thus S₁[x,u] ; :: thesis: verum

end;

consider seq being Function such that
A4: dom seq = NAT and
A5: rng seq c= REAL and
A6: for x being set st x in NAT holds
S₁[x,seq . x] from WELLORD2:sch 1(A2);
reconsider seq = seq as Real_Sequence by A4, A5, FUNCT_2:def 1, RELSET_1:11;
take seq ; :: thesis: ( rng seq c= X & seq is convergent & lim seq = r3 )
thus rng seq c= X :: thesis: ( seq is convergent & lim seq = r3 )

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
A7: ( x in dom seq & seq . x = y ) by FUNCT_1:def 5;
consider n being Nat such that
A8: ( x = n & seq . x = choose (X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[) ) by A6, A7;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
set n1 = n + 1;
set oi = ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[;
A9: r3 < r3 + (1 / (n + 1)) by XREAL_1:31;
then r3 - (1 / (n + 1)) < r3 by XREAL_1:21;
then r3 in ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[ by A9;
then not X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[ is empty by A1, Th38;
hence y in X by A7, A8, XBOOLE_0:def 4; :: thesis: verum

end;

A10: now

let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r3) < p )
assume A11: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r3) < p
set cp = [/(1 / p)\];
A12: 0 < 1 / p by A11;
A13: 1 / p <= [/(1 / p)\] by INT_1:def 5;
A14: 0 < [/(1 / p)\] by A12, INT_1:def 5;
then reconsider cp = [/(1 / p)\] as Element of NAT by INT_1:16;
take n = cp; :: thesis: for m being Element of NAT st n <= m holds
abs ((seq . m) - r3) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((seq . m) - r3) < p )
assume A15: n <= m ; :: thesis: abs ((seq . m) - r3) < p
consider m' being Nat such that
A16: ( m' = m & seq . m = choose (X /\ ].(r3 - (1 / (m' + 1))),(r3 + (1 / (m' + 1))).[) ) by A6;
set m1 = m + 1;
set oi = ].(r3 - (1 / (m + 1))),(r3 + (1 / (m + 1))).[;
A17: r3 < r3 + (1 / (m + 1)) by XREAL_1:31;
then r3 - (1 / (m + 1)) < r3 by XREAL_1:21;
then r3 in ].(r3 - (1 / (m + 1))),(r3 + (1 / (m + 1))).[ by A17;
then not X /\ ].(r3 - (1 / (m + 1))),(r3 + (1 / (m + 1))).[ is empty by A1, Th38;
then seq . m in ].(r3 - (1 / (m + 1))),(r3 + (1 / (m + 1))).[ by A16, XBOOLE_0:def 4;
then consider s being Real such that
A18: ( seq . m = s & r3 - (1 / (m + 1)) < s & s < r3 + (1 / (m + 1)) ) ;
( - (1 / (m + 1)) < s - r3 & s - r3 < 1 / (m + 1) ) by A18, XREAL_1:21, XREAL_1:22;
then A19: abs (s - r3) < 1 / (m + 1) by SEQ_2:9;
n + 1 <= m + 1 by A15, XREAL_1:8;
then A20: 1 / (m + 1) <= 1 / (n + 1) by XREAL_1:87;
n < n + 1 by NAT_1:13;
then A21: 1 / (n + 1) < 1 / n by A14, XREAL_1:90;
1 / (1 / p) >= 1 / cp by A12, A13, XREAL_1:87;
then 1 / n <= p ;
then 1 / (n + 1) < p by A21, XXREAL_0:2;
then 1 / (m + 1) < p by A20, XXREAL_0:2;
hence abs ((seq . m) - r3) < p by A18, A19, XXREAL_0:2; :: thesis: verum

end;

hence seq is convergent by SEQ_2:def 6; :: thesis: lim seq = r3
hence lim seq = r3 by A10, SEQ_2:def 7; :: thesis: verum