theorem Th39: :: DUALSP01:32

for X being RealNormSpace holds DualSp X is RealNormSpace