let n be Nat; :: thesis: for x1, x2, x3 being Element of REAL n holds |.(x2 - x1).| - |.(x2 - x3).| <= |.(x3 - x1).|
let x1, x2, x3 be Element of REAL n; :: thesis: |.(x2 - x1).| - |.(x2 - x3).| <= |.(x3 - x1).|
|.(x2 - x1).| = |.(x1 - x2).| by EUCLID:18;
then |.(x2 - x1).| - |.(x2 - x3).| <= |.(x1 - x3).| by Th3;
hence |.(x2 - x1).| - |.(x2 - x3).| <= |.(x3 - x1).| by EUCLID:18; :: thesis: verum