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