for N being Nat
for w1, w2 being Point of (TOP-REAL N) holds
( |.(w1 - w2).| = 0 iff w1 = w2 ) by Lm1, Lm2;