theorem :: EUCLID_2:33

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