for N being Nat
for w being Point of (TOP-REAL N) holds |.w.| >= 0 ;