let X be Subset of COMPLEX ; :: thesis: for z0 being Element of COMPLEX
for r being Element of REAL st X = { y where y is Complex : |.(y - z0).| < r } holds
X is open
let z0 be Element of COMPLEX ; :: thesis: for r being Element of REAL st X = { y where y is Complex : |.(y - z0).| < r } holds
X is open
let r be Element of REAL ; :: thesis: ( X = { y where y is Complex : |.(y - z0).| < r } implies X is open )
assume A1: X = { y where y is Complex : |.(y - z0).| < r } ; :: thesis: X is open
reconsider X0 = X as Subset of COMPLEX ;
for x being Complex st x in X0 holds
ex N being Neighbourhood of x st N c= X0

proof

let x be Complex; :: thesis: ( x in X0 implies ex N being Neighbourhood of x st N c= X0 )
assume x in X0 ; :: thesis: ex N being Neighbourhood of x st N c= X0
then A2: ex y being Complex st
( x = y & |.(y - z0).| < r ) by A1;
reconsider r1 = (r - |.(x - z0).|) / 2 as Real ;
A3: r - |.(x - z0).| > 0 by A2, XREAL_1:52;
set N = { y where y is Complex : |.(y - x).| < r1 } ;
reconsider N = { y where y is Complex : |.(y - x).| < r1 } as Neighbourhood of x by Th8, A3, XREAL_1:217;
take N ; :: thesis: N c= X0
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in N or z in X0 )
assume z in N ; :: thesis: z in X0
then consider y1 being Complex such that
A5: ( z = y1 & |.(y1 - x).| < r1 ) ;
A6: |.(y1 - z0).| <= |.(y1 - x).| + |.(x - z0).| by COMPLEX1:149;
A7: |.(y1 - x).| + |.(x - z0).| < r1 + |.(x - z0).| by A5, XREAL_1:10;
r1 < r - |.(x - z0).| by A3, XREAL_1:218;
then r1 + |.(x - z0).| < (r - |.(x - z0).|) + |.(x - z0).| by XREAL_1:10;
then |.(y1 - x).| + |.(x - z0).| < r by A7, XXREAL_0:2;
then |.(y1 - z0).| < r by A6, XXREAL_0:2;
hence z in X0 by A1, A5; :: thesis: verum

end;

hence X is open by Th14; :: thesis: verum