let X be Subset of REAL ; :: thesis: ( ( for r being real number 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 real number 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, Def5;
then consider s1 being Real_Sequence such that
A3: ( rng s1 c= X ` & s1 is convergent & not lim s1 in X ` ) by Def4;
lim s1 in X by A3, SUBSET_1:50;
then consider N being Neighbourhood of lim s1 such that
A4: N c= X by A1;
consider g being real number such that
A5: 0 < g and
A6: ].((lim s1) - g),((lim s1) + g).[ = N by Def7;
consider n being Element of NAT such that
A7: for m being Element of NAT st n <= m holds
abs ((s1 . m) - (lim s1)) < g by A3, A5, SEQ_2:def 7;
abs ((s1 . n) - (lim s1)) < g by A7;
then ( - g < (s1 . n) - (lim s1) & (s1 . n) - (lim s1) < g ) by SEQ_2:9;
then ( (lim s1) + (- g) < (lim s1) + ((s1 . n) - (lim s1)) & s1 . n < (lim s1) + g ) by XREAL_1:8, XREAL_1:21;
then A8: s1 . n in { s where s is Real : ( (lim s1) - g < s & s < (lim s1) + g ) } ;
n in NAT ;
then n in dom s1 by FUNCT_2:def 1;
then s1 . n in rng s1 by FUNCT_1:def 5;
hence contradiction by A3, A4, A6, A8, XBOOLE_0:def 5; :: thesis: verum