let S be RealNormSpace; :: thesis: for X being Subset of S st ( for r being Point of S st r in X holds

ex N being Neighbourhood of r st N c= X ) holds

X is open

let X be Subset of S; :: thesis: ( ( for r being Point of S st r in X holds

ex N being Neighbourhood of r st N c= X ) implies X is open )

assume that

A1: for r being Point of S st r in X holds

ex N being Neighbourhood of r st N c= X and

A2: not X is open ; :: thesis: contradiction

not X ` is closed by A2;

then consider s1 being sequence of S such that

A3: rng s1 c= X ` and

A4: s1 is convergent and

A5: not lim s1 in X ` ;

consider N being Neighbourhood of lim s1 such that

A6: N c= X by A1, A5, SUBSET_1:29;

consider g being Real such that

A7: 0 < g and

A8: { y where y is Point of S : ||.(y - (lim s1)).|| < g } c= N by NFCONT_1:def 1;

consider n being Nat such that

A9: for m being Nat st n <= m holds

||.((s1 . m) - (lim s1)).|| < g by A4, A7, NORMSP_1:def 7;

n in NAT by ORDINAL1:def 12;

then n in dom s1 by FUNCT_2:def 1;

then A10: s1 . n in rng s1 by FUNCT_1:def 3;

||.((s1 . n) - (lim s1)).|| < g by A9;

then s1 . n in { y where y is Point of S : ||.(y - (lim s1)).|| < g } ;

then s1 . n in N by A8;

hence contradiction by A3, A6, A10, XBOOLE_0:def 5; :: thesis: verum

ex N being Neighbourhood of r st N c= X ) holds

X is open

let X be Subset of S; :: thesis: ( ( for r being Point of S st r in X holds

ex N being Neighbourhood of r st N c= X ) implies X is open )

assume that

A1: for r being Point of S st r in X holds

ex N being Neighbourhood of r st N c= X and

A2: not X is open ; :: thesis: contradiction

not X ` is closed by A2;

then consider s1 being sequence of S such that

A3: rng s1 c= X ` and

A4: s1 is convergent and

A5: not lim s1 in X ` ;

consider N being Neighbourhood of lim s1 such that

A6: N c= X by A1, A5, SUBSET_1:29;

consider g being Real such that

A7: 0 < g and

A8: { y where y is Point of S : ||.(y - (lim s1)).|| < g } c= N by NFCONT_1:def 1;

consider n being Nat such that

A9: for m being Nat st n <= m holds

||.((s1 . m) - (lim s1)).|| < g by A4, A7, NORMSP_1:def 7;

n in NAT by ORDINAL1:def 12;

then n in dom s1 by FUNCT_2:def 1;

then A10: s1 . n in rng s1 by FUNCT_1:def 3;

||.((s1 . n) - (lim s1)).|| < g by A9;

then s1 . n in { y where y is Point of S : ||.(y - (lim s1)).|| < g } ;

then s1 . n in N by A8;

hence contradiction by A3, A6, A10, XBOOLE_0:def 5; :: thesis: verum