for n being Nat
for p being Point of (TOP-REAL n) holds
( |.p.| = 0 iff p = 0. (TOP-REAL n) ) by Th37, TOPRNS_1:24;