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 z in P ; :: thesis: dist y,z >= ((dist_min P) . x) - (dist x,y)
then (dist_min P) . x <= dist x,z by Th15;
then A1: (dist x,z) - (dist x,y) >= ((dist_min P) . x) - (dist x,y) by XREAL_1:15;
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:22;
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 Th16;
hence (dist_min P) . x <= (dist x,y) + ((dist_min P) . y) by XREAL_1:22; :: thesis: verum