let X be Subset of COMPLEX ; :: thesis: ( ( for z0 being Complex st z0 in X holds
ex N being Neighbourhood of z0 st N c= X ) implies X is open )
assume that
A1: for z0 being Complex st z0 in X holds
ex N being Neighbourhood of z0 st N c= X and
A2: not X is open ; :: thesis: contradiction
not X ` is closed by A2, Def11;
then consider s1 being Function of NAT ,COMPLEX such that
A3: rng s1 c= X ` and
A4: s1 is convergent and
A5: not lim s1 in X ` by Def10;
consider N being Neighbourhood of lim s1 such that
A6: N c= X by A1, A5, SUBSET_1:50;
consider g being Real such that
A7: 0 < g and
A8: { y where y is Complex : |.(y - (lim s1)).| < g } c= N by Def5;
consider n being Element of NAT such that
A9: for m being Element of NAT st n <= m holds
|.((s1 . m) - (lim s1)).| < g by A4, A7, COMSEQ_2:def 5;
n in NAT ;
then n in dom s1 by FUNCT_2:def 1;
then A10: s1 . n in rng s1 by FUNCT_1:def 5;
|.((s1 . n) - (lim s1)).| < g by A9;
then s1 . n in { y where y is Complex : |.(y - (lim s1)).| < g } ;
then s1 . n in N by A8;
hence contradiction by A3, A6, A10, XBOOLE_0:def 5; :: thesis: verum