let M be non empty MetrSpace; :: thesis: for P being non empty Subset of (TopSpaceMetr M)
for r being Real
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
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; :: 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) = lower_bound X by Th10;
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 st p in X holds
p >= r

proof

let p be Real; :: thesis: ( p in X implies p >= r )
assume p in X ; :: thesis: p >= r
then consider y being object such that
A4: y in dom (dist x) and
A5: y in P and
A6: (dist x) . y = p by A1, FUNCT_1:def 6;
reconsider y = y as Point of M by A4, TOPMETR:12;
p = dist (x,y) by A6, WEIERSTR:def 4;
hence p >= r by A3, A5; :: thesis: verum

end;

then lower_bound X >= r by SEQ_4:43;
hence (dist_min P) . x >= r by A2, WEIERSTR:def 6; :: thesis: verum