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