theorem Th33: :: DUALSP01:27

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