let X be ComplexUnitarySpace; :: thesis: for x, y being Point of X holds abs (||.x.|| - ||.y.||) <= ||.(x - y).||
let x, y be Point of X; :: thesis: abs (||.x.|| - ||.y.||) <= ||.(x - y).||
A1: ||.x.|| - ||.y.|| <= ||.(x - y).|| by Th50;
(y - x) + x = y - (x - x) by RLVECT_1:43
.= y - H₁(X) by RLVECT_1:28
.= y by RLVECT_1:26 ;
then ||.y.|| <= ||.(y - x).|| + ||.x.|| by Th48;
then ||.y.|| - ||.x.|| <= ||.(y - x).|| by XREAL_1:22;
then ||.y.|| - ||.x.|| <= ||.(- (x - y)).|| by RLVECT_1:47;
then ||.y.|| - ||.x.|| <= ||.(x - y).|| by Th49;
then - ||.(x - y).|| <= - (||.y.|| - ||.x.||) by XREAL_1:26;
hence abs (||.x.|| - ||.y.||) <= ||.(x - y).|| by A1, ABSVALUE:12; :: thesis: verum