:: deftheorem Def12 defines real_dist METRIC_1:def 12 :
for b₁ being Function of [:REAL,REAL:],REAL holds
( b₁ = real_dist iff for x, y being Real holds b₁ . (x,y) = |.(x - y).| );