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 )
consider X being non empty Subset of REAL such that
A1: X = (dist x) .: P and
A2: lower_bound ((dist x) .: P) = inf X by Th12;
assume A3: for y being Point of M st y in P holds
dist x,y >= r ; :: thesis: (dist_min P) . x >= r
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
A4: y in dom (dist x) and
A5: y in P and
A6: (dist x) . y = p by A1, FUNCT_1:def 12;
reconsider y = y as Point of M by A4, TOPMETR:16;
p = dist x,y by A6, WEIERSTR:def 6;
hence p >= r by A3, A5; :: thesis: verum

end;

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