let RNS be RealNormSpace; :: thesis: for x being Point of RNS holds 0 <= ||.x.||
let x be Point of RNS; :: thesis: 0 <= ||.x.||
||.(x - x).|| = ||.H₁(RNS).|| by RLVECT_1:15
.= 0 ;
then 0 <= (||.x.|| + ||.x.||) / 2 by Th3;
hence 0 <= ||.x.|| ; :: thesis: verum