theorem Th9: :: METRIC_1:9

for x, y being Element of REAL holds real_dist . (x,y) = real_dist . (y,x)