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 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

then A1: X ` is closed ;

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

defpred S_{1}[ Element of NAT , Point of S] means ( $2 in { y where y is Point of S : ||.(y - r).|| < 1 / ($1 + 1) } & $2 in X ` );

_{1}[n,s]

A11: for n being Element of NAT holds S_{1}[n,s1 . n]
from FUNCT_2:sch 3(A10);

A12: rng s1 c= X `

then lim s1 = r by A15, NORMSP_1:def 7;

then r in X ` by A22, A12, A1;

hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum

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 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

then A1: X ` is closed ;

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

defpred S

A4: now :: thesis: for g being Real st 0 < g holds

ex s being Point of S st

( s in { y where y is Point of S : ||.(y - r).|| < g } & s in X ` )

A10:
for n being Element of NAT ex s being Point of S st Sex s being Point of S st

( s in { y where y is Point of S : ||.(y - r).|| < g } & s in X ` )

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 object such that

A6: x in { y where y is Point of S : ||.(y - r).|| < g } and

A7: not x in X ;

consider s being Point of S such that

A8: x = s and

A9: ||.(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 A9; :: thesis: s in X `

thus s in X ` by A7, A8, XBOOLE_0:def 5; :: thesis: verum

end;( 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 object such that

A6: x in { y where y is Point of S : ||.(y - r).|| < g } and

A7: not x in X ;

consider s being Point of S such that

A8: x = s and

A9: ||.(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 A9; :: thesis: s in X `

thus s in X ` by A7, A8, XBOOLE_0:def 5; :: thesis: verum

proof

consider s1 being sequence of S such that
let n be Element of NAT ; :: thesis: ex s being Point of S st S_{1}[n,s]

0 < 1 * ((n + 1) ") ;

then 0 < 1 / (n + 1) by XCMPLX_0:def 9;

hence ex s being Point of S st S_{1}[n,s]
by A4; :: thesis: verum

end;0 < 1 * ((n + 1) ") ;

then 0 < 1 / (n + 1) by XCMPLX_0:def 9;

hence ex s being Point of S st S

A11: for n being Element of NAT holds S

A12: rng s1 c= X `

proof

let x be object ; :: 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 object such that

A13: y in dom s1 and

A14: s1 . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A13;

s1 . y in X ` by A11;

hence x in X ` by A14; :: thesis: verum

end;assume x in rng s1 ; :: thesis: x in X `

then consider y being object such that

A13: y in dom s1 and

A14: s1 . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A13;

s1 . y in X ` by A11;

hence x in X ` by A14; :: thesis: verum

A15: now :: thesis: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

||.((s1 . m) - r).|| < p

then A22:
s1 is convergent
;ex n being Nat st

for m being Nat st n <= m holds

||.((s1 . m) - r).|| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st

for m being Nat st n <= m holds

||.((s1 . m) - r).|| < p )

assume A16: 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

||.((s1 . m) - r).|| < p

consider n being Nat such that

A17: p " < n by SEQ_4:3;

(p ") + 0 < n + 1 by A17, XREAL_1:8;

then 1 / (n + 1) < 1 / (p ") by A16, XREAL_1:76;

then A18: 1 / (n + 1) < p by XCMPLX_1:216;

take n = n; :: thesis: for m being Nat st n <= m holds

||.((s1 . m) - r).|| < p

let m be Nat; :: thesis: ( n <= m implies ||.((s1 . m) - r).|| < p )

A19: m in NAT by ORDINAL1:def 12;

assume n <= m ; :: thesis: ||.((s1 . m) - r).|| < p

then A20: n + 1 <= m + 1 by XREAL_1:6;

s1 . m in { y where y is Point of S : ||.(y - r).|| < 1 / (m + 1) } by A11, A19;

then A21: ex y being Point of S st

( s1 . m = y & ||.(y - r).|| < 1 / (m + 1) ) ;

1 / (m + 1) <= 1 / (n + 1) by A20, XREAL_1:118;

then ||.((s1 . m) - r).|| < 1 / (n + 1) by A21, XXREAL_0:2;

hence ||.((s1 . m) - r).|| < p by A18, XXREAL_0:2; :: thesis: verum

end;for m being Nat st n <= m holds

||.((s1 . m) - r).|| < p )

assume A16: 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

||.((s1 . m) - r).|| < p

consider n being Nat such that

A17: p " < n by SEQ_4:3;

(p ") + 0 < n + 1 by A17, XREAL_1:8;

then 1 / (n + 1) < 1 / (p ") by A16, XREAL_1:76;

then A18: 1 / (n + 1) < p by XCMPLX_1:216;

take n = n; :: thesis: for m being Nat st n <= m holds

||.((s1 . m) - r).|| < p

let m be Nat; :: thesis: ( n <= m implies ||.((s1 . m) - r).|| < p )

A19: m in NAT by ORDINAL1:def 12;

assume n <= m ; :: thesis: ||.((s1 . m) - r).|| < p

then A20: n + 1 <= m + 1 by XREAL_1:6;

s1 . m in { y where y is Point of S : ||.(y - r).|| < 1 / (m + 1) } by A11, A19;

then A21: ex y being Point of S st

( s1 . m = y & ||.(y - r).|| < 1 / (m + 1) ) ;

1 / (m + 1) <= 1 / (n + 1) by A20, XREAL_1:118;

then ||.((s1 . m) - r).|| < 1 / (n + 1) by A21, XXREAL_0:2;

hence ||.((s1 . m) - r).|| < p by A18, XXREAL_0:2; :: thesis: verum

then lim s1 = r by A15, NORMSP_1:def 7;

then r in X ` by A22, A12, A1;

hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum