let n be Element of NAT ; :: thesis: for x1, x2, x3 being Element of REAL n holds |.(x1 - x2).| - |.(x2 - x3).| <= |.(x1 - x3).|
let x1, x2, x3 be Element of REAL n; :: thesis: |.(x1 - x2).| - |.(x2 - x3).| <= |.(x1 - x3).|
|.(x1 - x2).| <= |.(x1 - x3).| + |.(x3 - x2).| by EUCLID:22;
then |.(x1 - x2).| <= |.(x1 - x3).| + |.(x2 - x3).| by EUCLID:21;
then |.(x1 - x2).| - |.(x2 - x3).| <= (|.(x1 - x3).| + |.(x2 - x3).|) - |.(x2 - x3).| by XREAL_1:11;
hence |.(x1 - x2).| - |.(x2 - x3).| <= |.(x1 - x3).| ; :: thesis: verum