let M be non empty MetrSpace; :: thesis: for P being Subset of (TopSpaceMetr M)
for x being set st x in P holds
(dist_min P) . x = 0
let P be Subset of (TopSpaceMetr M); :: thesis: for x being set st x in P holds
(dist_min P) . x = 0
let x be set ; :: thesis: ( x in P implies (dist_min P) . x = 0 )
assume A1: x in P ; :: thesis: (dist_min P) . x = 0
then reconsider x = x as Point of M by TOPMETR:12;
set X = (dist x) .: P;
reconsider X = (dist x) .: P as non empty Subset of REAL by A1, TOPMETR:17;
lower_bound ((dist x) .: P) = lower_bound ([#] ((dist x) .: P)) by WEIERSTR:def 3
.= lower_bound X by WEIERSTR:def 1 ;
then A2: (dist_min P) . x = lower_bound X by WEIERSTR:def 6;
A3: for p being Real st p in X holds
p >= 0 by Th4;
for q being Real st ( for p being Real st p in X holds
p >= q ) holds
0 >= q by A1, Th3;
hence (dist_min P) . x = 0 by A2, A3, SEQ_4:44; :: thesis: verum