let S be RealNormSpace; :: thesis: for X being Subset of S st X is open holds
for r being Point of S st r in X holds
ex N being Neighbourhood of r st N c= X
let X be Subset of S; :: thesis: ( X is open implies for r being Point of S st r in X holds
ex N being Neighbourhood of r st N c= X )
assume A1: X is open ; :: thesis: for r being Point of S st r in X holds
ex N being Neighbourhood of r st N c= X
let r be Point of S; :: thesis: ( r in X implies ex N being Neighbourhood of r st N c= X )
assume that
A2: r in X and
A3: for N being Neighbourhood of r holds not N c= X ; :: thesis: contradiction

A4: now

let g be Real; :: thesis: ( 0 < g implies ex s being Point of S st
( s in { y where y is Point of S : ||.(y - r).|| < g } & s in X ` ) )
assume A5: 0 < g ; :: thesis: ex s being Point of S st
( s in { y where y is Point of S : ||.(y - r).|| < g } & s in X ` )
set N = { y where y is Point of S : ||.(y - r).|| < g } ;
{ y where y is Point of S : ||.(y - r).|| < g } is Neighbourhood of r by A5, NFCONT_1:3;
then not { y where y is Point of S : ||.(y - r).|| < g } c= X by A3;
then consider x being set such that
A6: ( x in { y where y is Point of S : ||.(y - r).|| < g } & not x in X ) by TARSKI:def 3;
consider s being Point of S such that
A7: ( x = s & ||.(s - r).|| < g ) by A6;
take s = s; :: thesis: ( s in { y where y is Point of S : ||.(y - r).|| < g } & s in X ` )
thus s in { y where y is Point of S : ||.(y - r).|| < g } by A7; :: thesis: s in X `
thus s in X ` by A6, A7, XBOOLE_0:def 5; :: thesis: verum

end;

defpred S₁[ Element of NAT , Point of S] means ( $2 in { y where y is Point of S : ||.(y - r).|| < 1 / ($1 + 1) } & $2 in X ` );
A8: for n being Element of NAT ex s being Point of S st S₁[n,s]

proof

let n be Element of NAT ; :: thesis: ex s being Point of S st S₁[n,s]
0 <= n by NAT_1:2;
then 0 + 0 < 1 + n ;
then 0 < 1 * ((n + 1) " ) ;
then 0 < 1 / (n + 1) by XCMPLX_0:def 9;
hence ex s being Point of S st S₁[n,s] by A4; :: thesis: verum

end;

consider s1 being sequence of S such that
A9: for n being Element of NAT holds S₁[n,s1 . n] from FUNCT_2:sch 3(A8);

A10: now

let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((s1 . m) - r).|| < p )
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((s1 . m) - r).|| < p
then A11: 0 < p " ;
consider n being Element of NAT such that
A12: p " < n by SEQ_4:10;
(p " ) + 0 < n + 1 by A12, XREAL_1:10;
then 1 / (n + 1) < 1 / (p " ) by A11, XREAL_1:78;
then A13: 1 / (n + 1) < p by XCMPLX_1:218;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
||.((s1 . m) - r).|| < p
let m be Element of NAT ; :: thesis: ( n <= m implies ||.((s1 . m) - r).|| < p )
assume n <= m ; :: thesis: ||.((s1 . m) - r).|| < p
then A14: n + 1 <= m + 1 by XREAL_1:8;
0 <= n by NAT_1:2;
then 0 + 0 < 1 + n ;
then A15: 1 / (m + 1) <= 1 / (n + 1) by A14, XREAL_1:120;
s1 . m in { y where y is Point of S : ||.(y - r).|| < 1 / (m + 1) } by A9;
then consider y being Point of S such that
A16: ( s1 . m = y & ||.(y - r).|| < 1 / (m + 1) ) ;
||.((s1 . m) - r).|| < 1 / (n + 1) by A15, A16, XXREAL_0:2;
hence ||.((s1 . m) - r).|| < p by A13, XXREAL_0:2; :: thesis: verum

end;

then A17: s1 is convergent by NORMSP_1:def 9;
then A18: lim s1 = r by A10, NORMSP_1:def 11;
A19: rng s1 c= X `

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng s1 or x in X ` )
assume x in rng s1 ; :: thesis: x in X `
then consider y being set such that
A20: y in dom s1 and
A21: s1 . y = x by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A20;
s1 . y in X ` by A9;
hence x in X ` by A21; :: thesis: verum

end;

X ` is closed by A1, NFCONT_1:def 6;
then r in X ` by A17, A18, A19, NFCONT_1:def 5;
hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum