let n be Nat; :: thesis: for x1, x2 being Element of REAL n holds |.(x1 - x2).| <= |.x1.| + |.x2.|
let x1, x2 be Element of REAL n; :: thesis: |.(x1 - x2).| <= |.x1.| + |.x2.|
|.(x1 - x2).| <= |.x1.| + |.(- x2).| by Th9;
hence |.(x1 - x2).| <= |.x1.| + |.x2.| by Th7; :: thesis: verum