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:15
.= 0 ;
then 0 <= (||.x.|| + ||.x.||) / 2 by Th104;
hence 0 <= ||.x.|| ; :: thesis: verum