theorem :: EUCLID_2:43

for n being Nat
for p being Point of (TOP-REAL n) holds
( p <> 0. (TOP-REAL n) iff |(p,p)| > 0 )