let M be non empty MetrSpace; :: thesis: for P being non empty Subset of (TopSpaceMetr M)
for x, y being Point of M holds (dist_min P) . x <= (dist (x,y)) + ((dist_min P) . y)
let P be non empty Subset of (TopSpaceMetr M); :: thesis: for x, y being Point of M holds (dist_min P) . x <= (dist (x,y)) + ((dist_min P) . y)
let x, y be Point of M; :: thesis: (dist_min P) . x <= (dist (x,y)) + ((dist_min P) . y)

now :: thesis: for z being Point of M st z in P holds
dist (y,z) >= ((dist_min P) . x) - (dist (x,y))

let z be Point of M; :: thesis: ( z in P implies dist (y,z) >= ((dist_min P) . x) - (dist (x,y)) )
assume z in P ; :: thesis: dist (y,z) >= ((dist_min P) . x) - (dist (x,y))
then (dist_min P) . x <= dist (x,z) by Th13;
then A1: (dist (x,z)) - (dist (x,y)) >= ((dist_min P) . x) - (dist (x,y)) by XREAL_1:13;
dist (x,z) <= (dist (x,y)) + (dist (y,z)) by METRIC_1:4;
then dist (y,z) >= (dist (x,z)) - (dist (x,y)) by XREAL_1:20;
hence dist (y,z) >= ((dist_min P) . x) - (dist (x,y)) by A1, XXREAL_0:2; :: thesis: verum

end;

then (dist_min P) . y >= ((dist_min P) . x) - (dist (x,y)) by Th14;
hence (dist_min P) . x <= (dist (x,y)) + ((dist_min P) . y) by XREAL_1:20; :: thesis: verum