let M be non empty MetrSpace; :: thesis: 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); :: thesis: 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; :: thesis: ( y in P implies (dist_min P) . x <= dist x,y )
assume A1: y in P ; :: thesis: (dist_min P) . x <= dist x,y
consider X being non empty Subset of REAL such that
A2: ( X = (dist x) .: P & lower_bound ((dist x) .: P) = inf X ) by Th12;
A3: (dist_min P) . x = inf X by A2, WEIERSTR:def 8;
A4: X is bounded_below by A2, Th14;
A5: dom (dist x) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
dist x,y = (dist x) . y by WEIERSTR:def 6;
then dist x,y in X by A1, A2, A5, FUNCT_1:def 12;
hence (dist_min P) . x <= dist x,y by A3, A4, SEQ_4:def 5; :: thesis: verum