let X be ComplexUnitarySpace; :: thesis: for x, y being Point of X holds ||.x.|| - ||.y.|| <= ||.(x - y).||
let x, y be Point of X; :: thesis: ||.x.|| - ||.y.|| <= ||.(x - y).||
(x - y) + y = x - (y - y) by RLVECT_1:29
.= x - H₁(X) by RLVECT_1:15
.= x by RLVECT_1:13 ;
then ||.x.|| <= ||.(x - y).|| + ||.y.|| by Th41;
hence ||.x.|| - ||.y.|| <= ||.(x - y).|| by XREAL_1:20; :: thesis: verum