let X be ComplexUnitarySpace; :: thesis: for x being Point of X holds 0 <= ||.x.||
let x be Point of X; :: thesis: 0 <= ||.x.||
0 <= Re (x .|. x) by Def11;
then 0 <= |.(x .|. x).| by Th29;
hence 0 <= ||.x.|| by SQUARE_1:def 2; :: thesis: verum