theorem Th4: :: NORMSP_1:4

for RNS being RealNormSpace
for x being Point of RNS holds 0 <= ||.x.||