let x, y be Element of REAL ; :: thesis: real_dist . (x,y) = real_dist . (y,x)
thus real_dist . (x,y) = abs (x - y) by Def13
.= abs (- (x - y)) by COMPLEX1:52
.= abs (y - x)
.= real_dist . (y,x) by Def13 ; :: thesis: verum