theorem Th1: :: HEINE:1

for x, y being Real
for A being SubSpace of RealSpace
for p, q being Point of A st x = p & y = q holds
dist (p,q) = |.(x - y).|