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 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 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 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:17;

hereby :: thesis: ( ( for r being Real 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 st r > 0 holds
ex p being Point of M st
( p in P & not dist (x,p) >= r )
let r be Real; :: 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 st p in X holds
p >= r

proof

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

end;

then A7: lower_bound X >= r by SEQ_4:43;
lower_bound ((dist x) .: P) = lower_bound ([#] ((dist x) .: P)) by WEIERSTR:def 3
.= lower_bound X by WEIERSTR:def 1 ;
hence contradiction by A1, A2, A7, WEIERSTR:def 6; :: thesis: verum

end;

A8: for p being Real st p in X holds
p >= 0

proof

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

end;

assume A11: for r being Real st r > 0 holds
ex p being Point of M st
( p in P & dist (x,p) < r ) ; :: thesis: (dist_min P) . x = 0
A12: for q being Real st ( for p being Real st p in X holds
p >= q ) holds
0 >= q

proof

let q be Real; :: thesis: ( ( for p being Real st p in X holds
p >= q ) implies 0 >= q )
assume A13: for z being Real st z in X holds
z >= q ; :: thesis: 0 >= q
assume 0 < q ; :: thesis: contradiction
then consider p being Point of M such that
A14: p in P and
A15: dist (x,p) < q by A11;
set z = (dist x) . p;
p in the carrier of (TopSpaceMetr M) by A14;
then p in dom (dist x) by FUNCT_2:def 1;
then A16: (dist x) . p in X by A14, FUNCT_1:def 6;
(dist x) . p < q by A15, WEIERSTR:def 4;
hence contradiction by A13, A16; :: thesis: verum

end;

lower_bound ((dist x) .: P) = lower_bound ([#] ((dist x) .: P)) by WEIERSTR:def 3
.= lower_bound X by WEIERSTR:def 1 ;
then lower_bound ((dist x) .: P) = 0 by A8, A12, SEQ_4:44;
hence (dist_min P) . x = 0 by WEIERSTR:def 6; :: thesis: verum