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:68;
hence |.(w1 + w2).| <= |.w1.| + |.w2.| by EUCLID:15; :: thesis: verum