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