let N be Element of NAT ; :: thesis: for w1, w2 being Point of (TOP-REAL N) holds |.w1.| - |.w2.| <= |.(w1 - w2).|
let w1, w2 be Point of (TOP-REAL N); :: thesis: |.w1.| - |.w2.| <= |.(w1 - w2).|
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:25;
w1 - w2 = s1 - s2 by EUCLID:73;
hence |.w1.| - |.w2.| <= |.(w1 - w2).| by EUCLID:18; :: thesis: verum