theorem :: TOPREAL6:93

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