let X be MetrSpace; :: thesis: for x, y, v, w being Element of X holds |.((dist (x,y)) - (dist (v,w))).| <= (dist (x,v)) + (dist (y,w))
let x, z, v, w be Element of X; :: thesis: |.((dist (x,z)) - (dist (v,w))).| <= (dist (x,v)) + (dist (z,w))
(dist (x,z)) - (dist (v,w)) = ((dist (x,z)) - (dist (v,z))) + ((dist (v,z)) - (dist (v,w))) ;
then A1: |.((dist (x,z)) - (dist (v,w))).| <= |.((dist (x,z)) - (dist (v,z))).| + |.((dist (v,z)) - (dist (v,w))).| by COMPLEX1:56;
A2: |.((dist (x,z)) - (dist (v,z))).| <= dist (x,v) by METRIC_6:1;
|.((dist (v,z)) - (dist (v,w))).| <= dist (z,w) by METRIC_6:1;
then |.((dist (x,z)) - (dist (v,z))).| + |.((dist (v,z)) - (dist (v,w))).| <= (dist (x,v)) + (dist (z,w)) by XREAL_1:7, A2;
hence |.((dist (x,z)) - (dist (v,w))).| <= (dist (x,v)) + (dist (z,w)) by A1, XXREAL_0:2; :: thesis: verum