for N being Nat
for w1, w2 being Point of (TOP-REAL N) holds |.(w1 + w2).| <= |.w1.| + |.w2.|