let X be Subset of REAL; :: thesis: ( ( for r being Element of REAL 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 Element of REAL 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 Real_Sequence such that
A3: rng s1 c= X ` and
A4: s1 is convergent and
A5: not lim s1 in X ` ;
reconsider ls = lim s1 as Element of REAL by XREAL_0:def 1;
consider N being Neighbourhood of ls such that
A6: N c= X by A1, A5, SUBSET_1:29;
consider g being Real such that
A7: 0 < g and
A8: ].((lim s1) - g),((lim s1) + g).[ = N by Def6;
consider n being Nat such that
A9: for m being Nat st n <= m holds
|.((s1 . m) - (lim s1)).| < g by A4, A7, SEQ_2: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;
A11: |.((s1 . n) - (lim s1)).| < g by A9;
then (s1 . n) - (lim s1) < g by SEQ_2:1;
then A12: s1 . n < (lim s1) + g by XREAL_1:19;
- g < (s1 . n) - (lim s1) by A11, SEQ_2:1;
then (lim s1) + (- g) < (lim s1) + ((s1 . n) - (lim s1)) by XREAL_1:6;
then s1 . n in { s where s is Real : ( (lim s1) - g < s & s < (lim s1) + g ) } by A12;
hence contradiction by A3, A6, A8, A10, XBOOLE_0:def 5; :: thesis: verum