theorem Th51: :: EUCLID_2:53

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