let X be Subset of COMPLEX; :: thesis: ( X is open implies for z0 being Complex st z0 in X holds
ex N being Neighbourhood of z0 st N c= X )
assume X is open ; :: thesis: for z0 being Complex st z0 in X holds
ex N being Neighbourhood of z0 st N c= X
then A1: X ` is closed ;
let z0 be Complex; :: thesis: ( z0 in X implies ex N being Neighbourhood of z0 st N c= X )
assume that
A2: z0 in X and
A3: for N being Neighbourhood of z0 holds not N c= X ; :: thesis: contradiction
defpred S<sub>1</sub>[ Nat, Complex] means ( $2 in { y where y is Complex : |.(y - z0).| < 1 / ($1 + 1) } & $2 in X ` );

now :: thesis: for g being Real st 0 < g holds
ex s being Element of COMPLEX st
( s in { y where y is Complex : |.(y - z0).| < g } & s in X ` )

let g be Real; :: thesis: ( 0 < g implies ex s being Element of COMPLEX st
( s in { y where y is Complex : |.(y - z0).| < g } & s in X ` ) )
assume A4: 0 < g ; :: thesis: ex s being Element of COMPLEX st
( s in { y where y is Complex : |.(y - z0).| < g } & s in X ` )
set N = { y where y is Complex : |.(y - z0).| < g } ;
{ y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0 by A4, Th6;
then not { y where y is Complex : |.(y - z0).| < g } c= X by A3;
then consider x being object such that
A5: x in { y where y is Complex : |.(y - z0).| < g } and
A6: not x in X ;
consider s being Complex such that
A7: x = s and
A8: |.(s - z0).| < g by A5;
reconsider s = s as Element of COMPLEX by XCMPLX_0:def 2;
take s = s; :: thesis: ( s in { y where y is Complex : |.(y - z0).| < g } & s in X ` )
thus s in { y where y is Complex : |.(y - z0).| < g } by A8; :: thesis: s in X `
thus s in X ` by A6, A7, XBOOLE_0:def 5; :: thesis: verum

end;

then A9: for n being Element of NAT ex s being Element of COMPLEX st S₁[n,s] ;
consider s1 being sequence of COMPLEX such that
A10: for n being Element of NAT holds S₁[n,s1 . n] from FUNCT_2:sch 3(A9);
A11: rng s1 c= X `

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng s1 or y in X ` )
assume y in rng s1 ; :: thesis: y in X `
then consider y1 being object such that
A12: y1 in dom s1 and
A13: s1 . y1 = y by FUNCT_1:def 3;
reconsider y1 = y1 as Element of NAT by A12;
s1 . y1 in X ` by A10;
hence y in X ` by A13; :: thesis: verum

end;

A14: 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) - z0).| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((s1 . m) - z0).| < p )
assume A15: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((s1 . m) - z0).| < p
consider n being Nat such that
A16: p " < n by SEQ_4:3;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((s1 . m) - z0).| < p
let m be Nat; :: thesis: ( n <= m implies |.((s1 . m) - z0).| < p )
assume n <= m ; :: thesis: |.((s1 . m) - z0).| < p
then n + 1 <= m + 1 by XREAL_1:6;
then A17: 1 / (m + 1) <= 1 / (n + 1) by XREAL_1:118;
m in NAT by ORDINAL1:def 12;
then s1 . m in { y where y is Complex : |.(y - z0).| < 1 / (m + 1) } by A10;
then ex y being Complex st
( s1 . m = y & |.(y - z0).| < 1 / (m + 1) ) ;
then A18: |.((s1 . m) - z0).| < 1 / (n + 1) by A17, XXREAL_0:2;
(p ") + 0 < n + 1 by A16, XREAL_1:8;
then 1 / (n + 1) < 1 / (p ") by A15, XREAL_1:76;
hence |.((s1 . m) - z0).| < p by A18, XXREAL_0:2; :: thesis: verum

end;

then A19: s1 is convergent ;
then lim s1 = z0 by A14, COMSEQ_2:def 6;
then z0 in COMPLEX \ X by A19, A11, A1;
hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum