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