let RNS be RealNormSpace; :: thesis: for x, y being Point of RNS holds abs (||.x.|| - ||.y.||) <= ||.(x - y).||
let x, y be Point of RNS; :: thesis: abs (||.x.|| - ||.y.||) <= ||.(x - y).||
(y - x) + x = y - (x - x) by RLVECT_1:29
.= y - H₁(RNS) by RLVECT_1:15
.= y by RLVECT_1:13 ;
then ||.y.|| <= ||.(y - x).|| + ||.x.|| by Def2;
then ||.y.|| - ||.x.|| <= ||.(y - x).|| by XREAL_1:20;
then ||.y.|| - ||.x.|| <= ||.(x - y).|| by Th11;
then A1: - (||.y.|| - ||.x.||) >= - ||.(x - y).|| by XREAL_1:24;
||.x.|| - ||.y.|| <= ||.(x - y).|| by Th12;
hence abs (||.x.|| - ||.y.||) <= ||.(x - y).|| by A1, ABSVALUE:5; :: thesis: verum