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 COMPLSP1:sch 1();
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, Th72; :: 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 Th65; :: thesis: verum

end;

A6: 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₁ )
thus for b₁ being set holds
( not b₁ in X or 0 <= b₁ ) by A5; :: thesis: verum

end;

thus dist x,A = lower_bound X by Def18
.= 0 by A2, A5, A6, A3, SEQ_4:def 5 ; :: thesis: verum