let X be RealUnitarySpace; :: thesis: for x, z, y being Point of X holds dist ((x - z),(y - z)) = dist (x,y)
let x, z, y be Point of X; :: thesis: dist ((x - z),(y - z)) = dist (x,y)
thus dist ((x - z),(y - z)) = ||.(((x - z) - y) + z).|| by RLVECT_1:43
.= ||.((x - (y + z)) + z).|| by RLVECT_1:41
.= ||.(((x - y) - z) + z).|| by RLVECT_1:41
.= ||.((x - y) - (z - z)).|| by RLVECT_1:43
.= ||.((x - y) - H₁(X)).|| by RLVECT_1:28
.= dist (x,y) by RLVECT_1:26 ; :: thesis: verum