let X be ComplexNormSpace; :: thesis: for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).||
let x, y be Point of X; :: thesis: ||.(x - y).|| = ||.(y - x).||
thus ||.(x - y).|| = ||.(- (x - y)).|| by CLVECT_1:104
.= ||.(y - x).|| by RLVECT_1:47 ; :: thesis: verum