let M be non empty MetrSpace; :: thesis: for P being non empty Subset of (TopSpaceMetr M)
for r being real number
for x being Point of M st ( for y being Point of M st y in P holds
dist x,y >= r ) holds
(dist_min P) . x >= r
let P be non empty Subset of (TopSpaceMetr M); :: thesis: for r being real number
for x being Point of M st ( for y being Point of M st y in P holds
dist x,y >= r ) holds
(dist_min P) . x >= r
let r be real number ; :: thesis: for x being Point of M st ( for y being Point of M st y in P holds
dist x,y >= r ) holds
(dist_min P) . x >= r
let x be Point of M; :: thesis: ( ( for y being Point of M st y in P holds
dist x,y >= r ) implies (dist_min P) . x >= r )
assume A1: for y being Point of M st y in P holds
dist x,y >= r ; :: thesis: (dist_min P) . x >= r
consider X being non empty Subset of REAL such that
A2: ( X = (dist x) .: P & lower_bound ((dist x) .: P) = inf X ) by Th12;
for p being real number st p in X holds
p >= r

proof

let p be real number ; :: thesis: ( p in X implies p >= r )
assume p in X ; :: thesis: p >= r
then consider y being set such that
A3: ( y in dom (dist x) & y in P & (dist x) . y = p ) by A2, FUNCT_1:def 12;
reconsider y = y as Point of M by A3, TOPMETR:16;
p = dist x,y by A3, WEIERSTR:def 6;
hence p >= r by A1, A3; :: thesis: verum

end;

then inf X >= r by SEQ_4:60;
hence (dist_min P) . x >= r by A2, WEIERSTR:def 8; :: thesis: verum