theorem Th43: :: DUALSP01:35

for X being RealNormSpace holds DualSp X is RealBanachSpace