for N being Nat
for w being Point of (TOP-REAL N) holds |.(- w).| = |.w.| by EUCLID:71;