let n be Element of 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 COMPLSP1:def 16 :: thesis: contradiction
A5: dist x,A = 0 by A2, A4, Th85;

now

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

proof

take 0 ; :: according to SEQ_4:def 2 :: thesis: for b₁ being set holds
( not b₁ in X or 0 <= b₁ )
let r be real number ; :: 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 ) ;
hence 0 <= r by Th65; :: thesis: verum

end;

0 + r = r ;
then consider r' being real number such that
A11: ( r' in X & r' < r ) by A5, A6, A7, A9, A10, SEQ_4:def 5;
consider z1 being Element of COMPLEX n such that
A12: ( r' = |.(x - z1).| & z1 in A ) by A11;
take z = z1 - x; :: thesis: ( |.z.| < r & x + z in A )
thus ( |.z.| < r & x + z in A ) by A11, A12, Th50, Th74; :: thesis: verum

end;

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