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
A2: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def 6;
set B = [#] ((dist p) .: C);
A3: [#] ((dist p) .: C) = (dist p) .: C by WEIERSTR:def 3;
A4: for s being real number st s in [#] ((dist p) .: C) holds
r <= s

proof

let s be real number ; :: thesis: ( s in [#] ((dist p) .: C) implies r <= s )
assume s in [#] ((dist p) .: C) ; :: thesis: r <= s
then consider y being set such that
y in dom (dist p) and
A5: y in C and
A6: s = (dist p) . y by A3, FUNCT_1:def 12;
reconsider y' = y as Point of M by A2, A5;
s = dist p,y' by A6, WEIERSTR:def 6;
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 A4, A3, SEQ_4:60;
then lower_bound ((dist p) .: C) >= r by WEIERSTR:def 5;
hence (dist_min C) . p >= r by WEIERSTR:def 8; :: thesis: verum