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

proof

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

end;

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