let X be RealUnitarySpace; :: thesis: for x being Point of X holds 0 <= ||.x.||
let x be Point of X; :: thesis: 0 <= ||.x.||
0 <= x .|. x by Def2;
hence 0 <= ||.x.|| by SQUARE_1:def 2; :: thesis: verum