let n be Nat; :: thesis: for x, x1, x2 being Element of REAL n holds |.(x1 - x2).| <= |.(x1 - x).| + |.(x - x2).|
let x, x1, x2 be Element of REAL n; :: thesis: |.(x1 - x2).| <= |.(x1 - x).| + |.(x - x2).|
reconsider R1 = x1, R2 = x2, R = x as Element of n -tuples_on REAL ;
|.(x1 - x2).| = |.(((R1 - R) + R) - R2).| by RVSUM_1:43
.= |.((x1 - x) + (x - x2)).| by RVSUM_1:40 ;
hence |.(x1 - x2).| <= |.(x1 - x).| + |.(x - x2).| by Th9; :: thesis: verum