theorem Th7: :: CARDFIL4:7

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