let n be Nat; :: thesis: for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st not x in A & A <> {} & A is closed holds
dist (x,A) > 0
let x be Element of COMPLEX n; :: thesis: for A being Subset of (COMPLEX n) st not x in A & A <> {} & A is closed holds
dist (x,A) > 0
let A be Subset of (COMPLEX n); :: thesis: ( not x in A & A <> {} & A is closed implies dist (x,A) > 0 )
assume that
A1: not x in A and
A2: A <> {} and
A3: for x being Element of COMPLEX n st ( for r being Real st r > 0 holds
ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A ) ) holds
x in A and
A4: dist (x,A) <= 0 ; :: according to SEQ_4:def 15 :: thesis: contradiction
A5: dist (x,A) = 0 by A2, A4, Th113;

now :: thesis: for r being Real st r > 0 holds
ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A )

deffunc H₁( Element of COMPLEX n) -> Element of REAL = In (|.(x - $1).|,REAL);
deffunc H₂( Element of COMPLEX n) -> Real = |.(x - $1).|;
defpred S₁[ set ] means $1 in A;
A6: for z being Element of COMPLEX n holds H₁(z) = H₂(z) ;
A7: { H₁(z1) where z1 is Element of COMPLEX n : S₁[z1] } = { H₂(z2) where z2 is Element of COMPLEX n : S₁[z2] } from FRAENKEL:sch 5(A6);
reconsider X = { H₁(z) where z is Element of COMPLEX n : S₁[z] } as Subset of REAL from DOMAIN_1:sch 8();
let r be Real; :: thesis: ( r > 0 implies ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A ) )
assume A8: r > 0 ; :: thesis: ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A )
consider z being Element of COMPLEX n such that
A9: z in A by A2, SUBSET_1:4;
A10: X is bounded_below

proof

take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of X
let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in X or 0 <= r )
assume r in X ; :: thesis: 0 <= r
then ex z being Element of COMPLEX n st
( r = |.(x - z).| & z in A ) by A7;
hence 0 <= r by Th94; :: thesis: verum

end;

A11: |.(x - z).| in X by A9, A7;
( dist (x,A) = lower_bound X & 0 + r = r ) by Def17, A7;
then consider r9 being Real such that
A12: r9 in X and
A13: r9 < r by A5, A8, A11, A10, Def2;
consider z1 being Element of COMPLEX n such that
A14: ( r9 = |.(x - z1).| & z1 in A ) by A12, A7;
take z = z1 - x; :: thesis: ( |.z.| < r & x + z in A )
thus ( |.z.| < r & x + z in A ) by A13, A14, Th79, Th103; :: thesis: verum

end;

hence contradiction by A1, A3; :: thesis: verum