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