let n be 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:19;
then |.(x1 - x2).| <= |.(x1 - x3).| + |.(x2 - x3).| by EUCLID:18;
then |.(x1 - x2).| - |.(x2 - x3).| <= (|.(x1 - x3).| + |.(x2 - x3).|) - |.(x2 - x3).| by XREAL_1:9;
hence |.(x1 - x2).| - |.(x2 - x3).| <= |.(x1 - x3).| ; :: thesis: verum