let X be MetrSpace; :: thesis: for x, z, y being Element of X holds abs ((dist (x,z)) - (dist (y,z))) <= dist (x,y)
let x, z, y be Element of X; :: thesis: abs ((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:22;
then A1: - (dist (x,y)) <= - ((dist (y,z)) - (dist (x,z))) by XREAL_1:26;
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:22;
hence abs ((dist (x,z)) - (dist (y,z))) <= dist (x,y) by A1, ABSVALUE:12; :: thesis: verum