theorem Th11: :: TOPMETR:11

for p, q being Point of RealSpace
for x, y being Real st x = p & y = q holds
dist (p,q) = |.(x - y).| by METRIC_1:def 12;