let X be open Subset of REAL ; :: thesis: for r being real number st r in X holds
ex N being Neighbourhood of r st N c= X
let r be real number ; :: thesis: ( r in X implies ex N being Neighbourhood of r st N c= X )
assume that
A1: r in X and
A2: for N being Neighbourhood of r holds not N c= X ; :: thesis: contradiction

A3: now

let N be Neighbourhood of r; :: thesis: ex s being Real st
( s in N & s in X ` )
not N c= X by A2;
then consider x being set such that
A4: ( x in N & not x in X ) by TARSKI:def 3;
consider g being real number such that
A5: ( 0 < g & N = ].(r - g),(r + g).[ ) by Def7;
consider s being Real such that
A6: ( x = s & r - g < s & s < r + g ) by A4, A5;
take s = s; :: thesis: ( s in N & s in X ` )
thus s in N by A4, A6; :: thesis: s in X `
thus s in X ` by A4, A6, XBOOLE_0:def 5; :: thesis: verum

end;

defpred S₁[ Element of NAT , real number ] means ( $2 in ].(r - (1 / ($1 + 1))),(r + (1 / ($1 + 1))).[ & $2 in X ` );
A7: for n being Element of NAT ex s being Real st S₁[n,s]

proof

let n be Element of NAT ; :: thesis: ex s being Real st S₁[n,s]
0 < 1 * ((n + 1) " ) ;
then 0 < 1 / (n + 1) by XCMPLX_0:def 9;
then reconsider N = ].(r - (1 / (n + 1))),(r + (1 / (n + 1))).[ as Neighbourhood of r by Def7;
ex s being Real st
( s in N & s in X ` ) by A3;
hence ex s being Real st S₁[n,s] ; :: thesis: verum

end;

deffunc H₁( Element of NAT ) -> Element of REAL = r - (1 / ($1 + 1));
consider s1 being Real_Sequence such that
A8: for n being Element of NAT holds s1 . n = H₁(n) from SEQ_1:sch 1();
deffunc H₂( Element of NAT ) -> Element of REAL = r + (1 / ($1 + 1));
consider s2 being Real_Sequence such that
A9: for n being Element of NAT holds s2 . n = H₂(n) from SEQ_1:sch 1();
consider s3 being Real_Sequence such that
A10: for n being Element of NAT holds S₁[n,s3 . n] from FUNCT_2:sch 3(A7);

A11: now

let s be real number ; :: thesis: ( 0 < s implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s1 . m) - r) < s )
assume 0 < s ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s1 . m) - r) < s
then A12: 0 < s " ;
consider n being Element of NAT such that
A13: s " < n by SEQ_4:10;
(s " ) + 0 < n + 1 by A13, XREAL_1:10;
then 1 / (n + 1) < 1 / (s " ) by A12, XREAL_1:78;
then A14: 1 / (n + 1) < s by XCMPLX_1:218;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
abs ((s1 . m) - r) < s
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((s1 . m) - r) < s )
assume n <= m ; :: thesis: abs ((s1 . m) - r) < s
then n + 1 <= m + 1 by XREAL_1:8;
then A15: 1 / (m + 1) <= 1 / (n + 1) by XREAL_1:120;
abs ((s1 . m) - r) = abs ((r - (1 / (m + 1))) - r) by A8
.= abs (- (1 / (m + 1)))
.= abs (1 / (m + 1)) by COMPLEX1:138
.= 1 / (m + 1) by ABSVALUE:def 1 ;
hence abs ((s1 . m) - r) < s by A14, A15, XXREAL_0:2; :: thesis: verum

end;

then A16: s1 is convergent by SEQ_2:def 6;
then A17: lim s1 = r by A11, SEQ_2:def 7;

A18: now

let s be real number ; :: thesis: ( 0 < s implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s2 . m) - r) < s )
assume 0 < s ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s2 . m) - r) < s
then A19: 0 < s " ;
consider n being Element of NAT such that
A20: s " < n by SEQ_4:10;
(s " ) + 0 < n + 1 by A20, XREAL_1:10;
then 1 / (n + 1) < 1 / (s " ) by A19, XREAL_1:78;
then A21: 1 / (n + 1) < s by XCMPLX_1:218;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
abs ((s2 . m) - r) < s
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((s2 . m) - r) < s )
assume n <= m ; :: thesis: abs ((s2 . m) - r) < s
then n + 1 <= m + 1 by XREAL_1:8;
then A22: 1 / (m + 1) <= 1 / (n + 1) by XREAL_1:120;
abs ((s2 . m) - r) = abs ((r + (1 / (m + 1))) - r) by A9
.= 1 / (m + 1) by ABSVALUE:def 1 ;
hence abs ((s2 . m) - r) < s by A21, A22, XXREAL_0:2; :: thesis: verum

end;

then A23: s2 is convergent by SEQ_2:def 6;
then A24: lim s2 = r by A18, SEQ_2:def 7;
A25: for n being Element of NAT holds
( s1 . n <= s3 . n & s3 . n <= s2 . n )

proof

let n be Element of NAT ; :: thesis: ( s1 . n <= s3 . n & s3 . n <= s2 . n )
s3 . n in ].(r - (1 / (n + 1))),(r + (1 / (n + 1))).[ by A10;
then A26: ex s being Real st
( s = s3 . n & r - (1 / (n + 1)) < s & s < r + (1 / (n + 1)) ) ;
hence s1 . n <= s3 . n by A8; :: thesis: s3 . n <= s2 . n
thus s3 . n <= s2 . n by A9, A26; :: thesis: verum

end;

then A27: s3 is convergent by A16, A17, A23, A24, SEQ_2:33;
A28: lim s3 = r by A16, A17, A23, A24, A25, SEQ_2:34;
A29: rng s3 c= X `

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng s3 or x in X ` )
assume x in rng s3 ; :: thesis: x in X `
then consider y being set such that
A30: y in dom s3 and
A31: s3 . y = x by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A30, FUNCT_2:def 1;
s3 . y in X ` by A10;
hence x in X ` by A31; :: thesis: verum

end;

X ` is closed by Def5;
then r in X ` by A27, A28, A29, Def4;
hence contradiction by A1, XBOOLE_0:def 5; :: thesis: verum