theorem Th73: :: DUALSP03:2

for X being strict RealNormSpace st DualSp X is separable holds
X is separable