theorem Th32: :: TOPRNS_1:32

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