let N be Element of NAT ; :: thesis: for w1, w2, w being Point of (TOP-REAL N) holds |.(w1 - w2).| <= |.(w1 - w).| + |.(w - w2).|
let w1, w2, w be Point of (TOP-REAL N); :: thesis: |.(w1 - w2).| <= |.(w1 - w).| + |.(w - w2).|
0. (TOP-REAL N) = w - w by EUCLID:46
.= (- w) + w by EUCLID:45 ;
then |.(w1 - w2).| = |.((w1 + ((- w) + w)) - w2).| by EUCLID:31
.= |.(((w1 + (- w)) + w) - w2).| by EUCLID:30
.= |.(((w1 - w) + w) - w2).| by EUCLID:45
.= |.((w1 - w) + (w - w2)).| by EUCLID:49 ;
hence |.(w1 - w2).| <= |.(w1 - w).| + |.(w - w2).| by Th30; :: thesis: verum