let X be ComplexUnitarySpace; for x, y, z being Point of X holds dist ((x - z),(y - z)) = dist (x,y)
let x, y, z be Point of X; dist ((x - z),(y - z)) = dist (x,y)
thus dist ((x - z),(y - z)) =
||.(((x - z) - y) + z).||
by RLVECT_1:29
.=
||.((x - (y + z)) + z).||
by RLVECT_1:27
.=
||.(((x - y) - z) + z).||
by RLVECT_1:27
.=
||.((x - y) - (z - z)).||
by RLVECT_1:29
.=
||.((x - y) - H1(X)).||
by RLVECT_1:15
.=
dist (x,y)
by RLVECT_1:13
; verum