let X be MetrSpace; :: thesis: for x, y, z being Element of X holds |.((dist (x,z)) - (dist (y,z))).| <= dist (x,y)
let x, y, z be Element of X; :: thesis: |.((dist (x,z)) - (dist (y,z))).| <= dist (x,y)
dist (y,z) <= (dist (y,x)) + (dist (x,z)) by METRIC_1:4;
then (dist (y,z)) - (dist (x,z)) <= dist (x,y) by XREAL_1:20;
then A1: - (dist (x,y)) <= - ((dist (y,z)) - (dist (x,z))) by XREAL_1:24;
dist (x,z) <= (dist (x,y)) + (dist (y,z)) by METRIC_1:4;
then (dist (x,z)) - (dist (y,z)) <= dist (x,y) by XREAL_1:20;
hence |.((dist (x,z)) - (dist (y,z))).| <= dist (x,y) by A1, ABSVALUE:5; :: thesis: verum