let X be open Subset of REAL; :: thesis: for r being Real st r in X holds
ex N being Neighbourhood of r st N c= X
let r be Real; :: 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
defpred S₁[ Nat, Real] means ( $2 in ].(r - (1 / ($1 + 1))),(r + (1 / ($1 + 1))).[ & $2 in X ` );

A3: now :: thesis: for N being Neighbourhood of r ex s being Element of REAL st
( s in N & s in X ` )

let N be Neighbourhood of r; :: thesis: ex s being Element of REAL st
( s in N & s in X ` )
consider g being Real such that
0 < g and
A4: N = ].(r - g),(r + g).[ by Def6;
not N c= X by A2;
then consider x being object such that
A5: x in N and
A6: not x in X ;
consider s being Real such that
A7: x = s and
r - g < s and
s < r + g by A5, A4;
reconsider s = s as Element of REAL by XREAL_0:def 1;
take s = s; :: thesis: ( s in N & s in X ` )
thus s in N by A5, A7; :: thesis: s in X `
thus s in X ` by A6, A7, XBOOLE_0:def 5; :: thesis: verum

end;

A8: for n being Element of NAT ex s being Element of REAL st S₁[n,s]

proof

let n be Element of NAT ; :: thesis: ex s being Element of 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 Def6;
ex s being Element of REAL st
( s in N & s in X ` ) by A3;
hence ex s being Element of REAL st S₁[n,s] ; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( s1 . n <= s3 . n & s3 . n <= s2 . n )
n in NAT by ORDINAL1:def 12;
then s3 . n in ].(r - (1 / (n + 1))),(r + (1 / (n + 1))).[ by A9;
then A13: ex s being Real st
( s = s3 . n & r - (1 / (n + 1)) < s & s < r + (1 / (n + 1)) ) ;
hence s1 . n <= s3 . n by A10; :: thesis: s3 . n <= s2 . n
thus s3 . n <= s2 . n by A11, A13; :: thesis: verum

end;

A14: rng s3 c= X `

proof

let x be object ; :: 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 object such that
A15: y in dom s3 and
A16: s3 . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A15, FUNCT_2:def 1;
s3 . y in X ` by A9;
hence x in X ` by A16; :: thesis: verum

end;

A17: X ` is closed by Def5;

A18: now :: thesis: for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
|.((s2 . m) - r).| < s

let s be Real; :: thesis: ( 0 < s implies ex n being Nat st
for m being Nat st n <= m holds
|.((s2 . m) - r).| < s )
assume A19: 0 < s ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((s2 . m) - r).| < s
consider n being Nat such that
A20: s " < n by SEQ_4:3;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((s2 . m) - r).| < s
let m be Nat; :: thesis: ( n <= m implies |.((s2 . m) - r).| < s )
assume n <= m ; :: thesis: |.((s2 . m) - r).| < s
then n + 1 <= m + 1 by XREAL_1:6;
then A21: 1 / (m + 1) <= 1 / (n + 1) by XREAL_1:118;
(s ") + 0 < n + 1 by A20, XREAL_1:8;
then 1 / (n + 1) < 1 / (s ") by A19, XREAL_1:76;
then A22: 1 / (n + 1) < s by XCMPLX_1:216;
|.((s2 . m) - r).| = |.((r + (1 / (m + 1))) - r).| by A11
.= 1 / (m + 1) by ABSVALUE:def 1 ;
hence |.((s2 . m) - r).| < s by A22, A21, XXREAL_0:2; :: thesis: verum

end;

then A23: s2 is convergent ;
then A24: lim s2 = r by A18, SEQ_2:def 7;

A25: now :: thesis: for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
|.((s1 . m) - r).| < s

let s be Real; :: thesis: ( 0 < s implies ex n being Nat st
for m being Nat st n <= m holds
|.((s1 . m) - r).| < s )
assume A26: 0 < s ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((s1 . m) - r).| < s
consider n being Nat such that
A27: s " < n by SEQ_4:3;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((s1 . m) - r).| < s
let m be Nat; :: thesis: ( n <= m implies |.((s1 . m) - r).| < s )
assume n <= m ; :: thesis: |.((s1 . m) - r).| < s
then n + 1 <= m + 1 by XREAL_1:6;
then A28: 1 / (m + 1) <= 1 / (n + 1) by XREAL_1:118;
(s ") + 0 < n + 1 by A27, XREAL_1:8;
then 1 / (n + 1) < 1 / (s ") by A26, XREAL_1:76;
then A29: 1 / (n + 1) < s by XCMPLX_1:216;
|.((s1 . m) - r).| = |.((r - (1 / (m + 1))) - r).| by A10
.= |.(- (1 / (m + 1))).|
.= |.(1 / (m + 1)).| by COMPLEX1:52
.= 1 / (m + 1) by ABSVALUE:def 1 ;
hence |.((s1 . m) - r).| < s by A29, A28, XXREAL_0:2; :: thesis: verum

end;

then A30: s1 is convergent ;
then lim s1 = r by A25, SEQ_2:def 7;
then ( s3 is convergent & lim s3 = r ) by A30, A23, A24, A12, SEQ_2:19, SEQ_2:20;
then r in X ` by A14, A17;
hence contradiction by A1, XBOOLE_0:def 5; :: thesis: verum