theorem Th9: :: COUSIN:12

for n being Nat
for x, y being Element of (Euclid n)
for g, h being Point of (REAL-NS n) st x = g & y = h holds
dist (x,y) = ||.(g - h).||