theorem Th6: :: CARDFIL4:6

for x, y being Point of RealSpace ex xr, yr being Real st
( x = xr & y = yr & dist (x,y) = real_dist . (x,y) & dist (x,y) = (Pitag_dist 1) . (<*x*>,<*y*>) & dist (x,y) = |.(xr - yr).| )