let n be Element of 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) -> 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();
assume A1: x in A ; :: thesis: dist (x,A) = 0
then A2: |.(x - x).| in X ;

A3: now

reconsider r = |.(x - x).| as real number ;
let r1 be real number ; :: thesis: ( 0 < r1 implies ex r being real number st
( r in X & r < 0 + r1 ) )
assume A4: 0 < r1 ; :: thesis: ex r being real number st
( r in X & r < 0 + r1 )
take r = r; :: thesis: ( r in X & r < 0 + r1 )
thus r in X by A1; :: thesis: r < 0 + r1
thus r < 0 + r1 by A4, Th119; :: thesis: verum

end;

A5: now

let r be real number ; :: 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 ) ;
hence 0 <= r by Th112; :: thesis: verum

end;

A6: X is bounded_below

proof

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

end;

thus dist (x,A) = lower_bound X by Def20
.= 0 by A2, A5, A6, A3, Def5 ; :: thesis: verum