theorem Th8: :: CARDFIL4:8

for x, y being Point of (Euclid 1)
for r, s being Real st x = <*r*> & y = <*s*> holds
dist (x,y) = |.(r - s).|