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:43
.= x - H₁(X) by RLVECT_1:28
.= x by RLVECT_1:26 ;
then ||.x.|| <= ||.(x - y).|| + ||.y.|| by Th48;
hence ||.x.|| - ||.y.|| <= ||.(x - y).|| by XREAL_1:22; :: thesis: verum