let x, y be Point of X; :: thesis: dist (x,y) = dist (y,x)
thus dist (x,y) = ||.(- (y - x)).|| by RLVECT_1:33
.= dist (y,x) by Th42 ; :: thesis: verum