theorem Th39: :: EUCLID_2:41

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