let M be non empty MetrSpace; :: thesis: for P being non empty Subset of (TopSpaceMetr M)
for x being Point of M holds
( (dist_min P) . x = 0 iff for r being real number st r > 0 holds
ex p being Point of M st
( p in P & dist x,p < r ) )
let P be non empty Subset of (TopSpaceMetr M); :: thesis: for x being Point of M holds
( (dist_min P) . x = 0 iff for r being real number st r > 0 holds
ex p being Point of M st
( p in P & dist x,p < r ) )
let x be Point of M; :: thesis: ( (dist_min P) . x = 0 iff for r being real number st r > 0 holds
ex p being Point of M st
( p in P & dist x,p < r ) )
reconsider X = (dist x) .: P as non empty Subset of REAL by TOPMETR:24;

hereby :: thesis: ( ( for r being real number st r > 0 holds
ex p being Point of M st
( p in P & dist x,p < r ) ) implies (dist_min P) . x = 0 )

assume A1: (dist_min P) . x = 0 ; :: thesis: for r being real number st r > 0 holds
ex p being Point of M st
( p in P & not dist x,p >= r )
let r be real number ; :: thesis: ( r > 0 implies ex p being Point of M st
( p in P & not dist x,p >= r ) )
assume A2: r > 0 ; :: thesis: ex p being Point of M st
( p in P & not dist x,p >= r )
assume A3: for p being Point of M st p in P holds
dist x,p >= r ; :: thesis: contradiction
for p being real number st p in X holds
p >= r

proof

let p be real number ; :: thesis: ( p in X implies p >= r )
assume p in X ; :: thesis: p >= r
then consider y being set such that
A4: ( y in dom (dist x) & y in P & p = (dist x) . y ) by FUNCT_1:def 12;
reconsider z = y as Point of M by A4, TOPMETR:16;
dist x,z >= r by A3, A4;
hence p >= r by A4, WEIERSTR:def 6; :: thesis: verum

end;

then A5: lower_bound X >= r by SEQ_4:60;
lower_bound ((dist x) .: P) = lower_bound ([#] ((dist x) .: P)) by WEIERSTR:def 5
.= lower_bound X by WEIERSTR:def 3 ;
hence contradiction by A1, A2, A5, WEIERSTR:def 8; :: thesis: verum

end;

assume A6: for r being real number st r > 0 holds
ex p being Point of M st
( p in P & dist x,p < r ) ; :: thesis: (dist_min P) . x = 0
A7: lower_bound ((dist x) .: P) = lower_bound ([#] ((dist x) .: P)) by WEIERSTR:def 5
.= lower_bound X by WEIERSTR:def 3 ;
A8: for p being real number st p in X holds
p >= 0

proof

let p be real number ; :: thesis: ( p in X implies p >= 0 )
assume p in X ; :: thesis: p >= 0
then consider y being set such that
A9: ( y in dom (dist x) & y in P & p = (dist x) . y ) by FUNCT_1:def 12;
reconsider z = y as Point of M by A9, TOPMETR:16;
dist x,z >= 0 by METRIC_1:5;
hence p >= 0 by A9, WEIERSTR:def 6; :: thesis: verum

end;

for q being real number st ( for p being real number st p in X holds
p >= q ) holds
0 >= q

proof

let q be real number ; :: thesis: ( ( for p being real number st p in X holds
p >= q ) implies 0 >= q )
assume A10: for z being real number st z in X holds
z >= q ; :: thesis: 0 >= q
assume 0 < q ; :: thesis: contradiction
then consider p being Point of M such that
A11: ( p in P & dist x,p < q ) by A6;
A12: (dist x) . p < q by A11, WEIERSTR:def 6;
set z = (dist x) . p;
p in the carrier of (TopSpaceMetr M) by A11;
then p in dom (dist x) by FUNCT_2:def 1;
then (dist x) . p in X by A11, FUNCT_1:def 12;
hence contradiction by A10, A12; :: thesis: verum

end;

then lower_bound ((dist x) .: P) = 0 by A7, A8, SEQ_4:61;
hence (dist_min P) . x = 0 by WEIERSTR:def 8; :: thesis: verum