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:138
.= abs (y - x)
.= real_dist . y,x by Def13 ; :: thesis: verum