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