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