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

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

end;

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