theorem Th27: :: DUALSP04:18

for X being RealUnitarySpace
for f being Point of (DualSp X) holds 0 <= ||.f.||