theorem Th53: :: EUCLID_2:55

for n being Nat
for p being Point of (TOP-REAL n) holds
( p,p are_orthogonal iff p = 0. (TOP-REAL n) ) by Th39;