let CNS be ComplexNormSpace; :: thesis: for x being Point of CNS holds 0 <= ||.x.||
let x be Point of CNS; :: thesis: 0 <= ||.x.||
||.(x - x).|| = ||.H₁(CNS).|| by RLVECT_1:28
.= 0 by Def11 ;
then 0 <= (||.x.|| + ||.x.||) / 2 by Th105;
hence 0 <= ||.x.|| ; :: thesis: verum