let n be Nat; :: thesis: for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st x in A holds
dist (x,A) = 0
let x be Element of COMPLEX n; :: thesis: for A being Subset of (COMPLEX n) st x in A holds
dist (x,A) = 0
let A be Subset of (COMPLEX n); :: thesis: ( x in A implies dist (x,A) = 0 )
defpred S₁[ set ] means $1 in A;
deffunc H₁( Element of COMPLEX n) -> Element of REAL = In (|.(x - $1).|,REAL);
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 DOMAIN_1:sch 8();
A1: for z being Element of COMPLEX n holds H₁(z) = H₂(z) ;
A2: { 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(A1);
assume A3: x in A ; :: thesis: dist (x,A) = 0
then A4: |.(x - x).| in X by A2;

A5: now :: thesis: for r1 being Real st 0 < r1 holds
ex r being Real st
( r in X & r < 0 + r1 )

reconsider r = |.(x - x).| as Real ;
let r1 be Real; :: thesis: ( 0 < r1 implies ex r being Real st
( r in X & r < 0 + r1 ) )
assume A6: 0 < r1 ; :: thesis: ex r being Real st
( r in X & r < 0 + r1 )
take r = r; :: thesis: ( r in X & r < 0 + r1 )
thus r in X by A3, A2; :: thesis: r < 0 + r1
thus r < 0 + r1 by A6, Th101; :: thesis: verum

end;

A7: now :: thesis: for r being Real st r in X holds
0 <= r

let r be Real; :: thesis: ( r in X implies 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 A2;
hence 0 <= r by Th94; :: thesis: verum

end;

A8: X is bounded_below

proof

take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of X
let x be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not x in X or 0 <= x )
thus ( not x in X or 0 <= x ) by A7; :: thesis: verum

end;

thus dist (x,A) = lower_bound X by Def17, A2
.= 0 by A4, A7, A8, A5, Def2 ; :: thesis: verum