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