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 Def13;
then 0 <= |.(x .|. x).| by Th36;
hence 0 <= ||.x.|| by SQUARE_1:def 2; :: thesis: verum