let M be non empty MetrSpace; for P being non empty Subset of (TopSpaceMetr M)
for x, y being Point of M st y in P holds
(dist_min P) . x <= dist (x,y)
let P be non empty Subset of (TopSpaceMetr M); for x, y being Point of M st y in P holds
(dist_min P) . x <= dist (x,y)
let x, y be Point of M; ( y in P implies (dist_min P) . x <= dist (x,y) )
A1:
( dom (dist x) = the carrier of (TopSpaceMetr M) & dist (x,y) = (dist x) . y )
by FUNCT_2:def 1, WEIERSTR:def 4;
consider X being non empty Subset of REAL such that
A2:
X = (dist x) .: P
and
A3:
lower_bound ((dist x) .: P) = lower_bound X
by Th10;
assume
y in P
; (dist_min P) . x <= dist (x,y)
then A4:
dist (x,y) in X
by A2, A1, FUNCT_1:def 6;
( (dist_min P) . x = lower_bound X & X is bounded_below )
by A2, A3, Th12, WEIERSTR:def 6;
hence
(dist_min P) . x <= dist (x,y)
by A4, SEQ_4:def 2; verum