let RNS be RealNormSpace; :: thesis: for x, y being Point of RNS holds ||.(x - y).|| = ||.(y - x).||
let x, y be Point of RNS; :: thesis: ||.(x - y).|| = ||.(y - x).||
x - y = - (y - x) by RLVECT_1:33;
hence ||.(x - y).|| = ||.(y - x).|| by Th2; :: thesis: verum