theorem Th3: :: JORDAN2C:9

for n being Nat
for q1, q2 being Point of (TOP-REAL n) holds |.(|.q1.| - |.q2.|).| <= |.(q1 - q2).|