theorem Th28: :: BHSP_1:28

for X being RealUnitarySpace
for x being Point of X holds 0 <= ||.x.||