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
A1: dist x,z <= (dist x,y) + (dist y,z) by METRIC_1:4;
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 - (dist x,y) <= - ((dist y,z) - (dist x,z)) by XREAL_1:26;
then ( - (dist x,y) <= (dist x,z) - (dist y,z) & (dist x,z) - (dist y,z) <= dist x,y ) by A1, XREAL_1:22;
hence abs ((dist x,z) - (dist y,z)) <= dist x,y by ABSVALUE:12; :: thesis: verum