let M be non empty MetrSpace; :: thesis: for C being non empty Subset of (TopSpaceMetr M)
for p being Point of (TopSpaceMetr M) holds (dist_min C) . p >= 0
let C be non empty Subset of (TopSpaceMetr M); :: thesis: for p being Point of (TopSpaceMetr M) holds (dist_min C) . p >= 0
let p be Point of (TopSpaceMetr M); :: thesis: (dist_min C) . p >= 0
A1: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def 5;
then reconsider x = p as Point of M ;
set B = [#] ((dist x) .: C);
A2: [#] ((dist x) .: C) = (dist x) .: C by WEIERSTR:def 1;
A3: for r being Real st r in [#] ((dist x) .: C) holds
0 <= r

proof

let r be Real; :: thesis: ( r in [#] ((dist x) .: C) implies 0 <= r )
assume r in [#] ((dist x) .: C) ; :: thesis: 0 <= r
then consider y being object such that
y in dom (dist x) and
A4: y in C and
A5: r = (dist x) . y by A2, FUNCT_1:def 6;
reconsider y9 = y as Point of M by A1, A4;
r = dist (x,y9) by A5, WEIERSTR:def 4;
hence 0 <= r by METRIC_1:5; :: thesis: verum

end;

dom (dist x) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
then lower_bound ([#] ((dist x) .: C)) >= 0 by A2, A3, SEQ_4:43;
then lower_bound ((dist x) .: C) >= 0 by WEIERSTR:def 3;
hence (dist_min C) . p >= 0 by WEIERSTR:def 6; :: thesis: verum