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 ) )
defpred S₁[ object , object ] means ex n being Nat st
( $1 = n & $2 = the Element of X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[ );
assume A1: r3 in Cl X ; :: thesis: ex seq being Real_Sequence st
( rng seq c= X & seq is convergent & lim seq = r3 )

A2: now :: thesis: for x being object st x in NAT holds
ex u being object st
( u in REAL & S₁[x,u] )

let x be object ; :: thesis: ( x in NAT implies ex u being object st
( u in REAL & S₁[x,u] ) )
assume x in NAT ; :: thesis: ex u being object 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 = the Element of X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[ as object ;
take u = u; :: thesis: ( u in REAL & S₁[x,u] )
A3: r3 < r3 + (1 / (n + 1)) by XREAL_1:29;
then r3 - (1 / (n + 1)) < r3 by XREAL_1:19;
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, Th63;
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 & rng seq c= REAL ) and
A5: 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 by A4, FUNCT_2:def 1, RELSET_1:4;
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 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
A6: x in dom seq and
A7: seq . x = y by FUNCT_1:def 3;
consider n being Nat such that
x = n and
A8: seq . x = the Element of X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[ by A5, A6;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
set n1 = n + 1;
set oi = ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[;
A9: r3 < r3 + (1 / (n + 1)) by XREAL_1:29;
then r3 - (1 / (n + 1)) < r3 by XREAL_1:19;
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, Th63;
hence y in X by A7, A8, XBOOLE_0:def 4; :: thesis: verum

end;

A10: now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - r3).| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - r3).| < p )
set cp = [/(1 / p)\];
A11: 1 / p <= [/(1 / p)\] by INT_1:def 7;
assume A12: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - r3).| < p
then A13: 0 < [/(1 / p)\] by INT_1:def 7;
then reconsider cp = [/(1 / p)\] as Element of NAT by INT_1:3;
reconsider n = cp as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((seq . m) - r3).| < p
n < n + 1 by NAT_1:13;
then A14: 1 / (n + 1) < 1 / n by A13, XREAL_1:88;
1 / (1 / p) >= 1 / cp by A12, A11, XREAL_1:85;
then A15: 1 / (n + 1) < p by A14, XXREAL_0:2;
let m be Nat; :: thesis: ( n <= m implies |.((seq . m) - r3).| < p )
assume n <= m ; :: thesis: |.((seq . m) - r3).| < p
then A16: n + 1 <= m + 1 by XREAL_1:6;
set m1 = m + 1;
1 / (m + 1) <= 1 / (n + 1) by A16, XREAL_1:85;
then A17: 1 / (m + 1) < p by A15, XXREAL_0:2;
set oi = ].(r3 - (1 / (m + 1))),(r3 + (1 / (m + 1))).[;
A18: r3 < r3 + (1 / (m + 1)) by XREAL_1:29;
then r3 - (1 / (m + 1)) < r3 by XREAL_1:19;
then r3 in ].(r3 - (1 / (m + 1))),(r3 + (1 / (m + 1))).[ by A18;
then A19: not X /\ ].(r3 - (1 / (m + 1))),(r3 + (1 / (m + 1))).[ is empty by A1, Th63;
m in NAT by ORDINAL1:def 12;
then ex m9 being Nat st
( m9 = m & seq . m = the Element of X /\ ].(r3 - (1 / (m9 + 1))),(r3 + (1 / (m9 + 1))).[ ) by A5;
then seq . m in ].(r3 - (1 / (m + 1))),(r3 + (1 / (m + 1))).[ by A19, XBOOLE_0:def 4;
then consider s being Real such that
A20: seq . m = s and
A21: ( r3 - (1 / (m + 1)) < s & s < r3 + (1 / (m + 1)) ) ;
( - (1 / (m + 1)) < s - r3 & s - r3 < 1 / (m + 1) ) by A21, XREAL_1:19, XREAL_1:20;
then |.(s - r3).| < 1 / (m + 1) by SEQ_2:1;
hence |.((seq . m) - r3).| < p by A20, A17, XXREAL_0:2; :: thesis: verum

end;

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