let N be Nat; :: thesis: for w, w1, w2 being Point of (TOP-REAL N) holds |.(w1 - w2).| <= |.(w1 - w).| + |.(w - w2).|
let w, w1, w2 be Point of (TOP-REAL N); :: thesis: |.(w1 - w2).| <= |.(w1 - w).| + |.(w - w2).|
0. (TOP-REAL N) = w - w by RLVECT_1:5
.= (- w) + w ;
then |.(w1 - w2).| = |.((w1 + ((- w) + w)) - w2).| by RLVECT_1:4
.= |.(((w1 + (- w)) + w) - w2).| by RLVECT_1:def 3
.= |.(((w1 - w) + w) - w2).|
.= |.((w1 - w) + (w - w2)).| by RLVECT_1:def 3 ;
hence |.(w1 - w2).| <= |.(w1 - w).| + |.(w - w2).| by Th29; :: thesis: verum