for n being Nat
for q being Point of (TOP-REAL n) holds |.|.q.|.| = |.q.| by ABSVALUE:def 1;