let X be ComplexUnitarySpace; :: thesis: for x, y being Point of X holds dist x,y = dist y,x
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