theorem :: NORMSP_4:25

for X being RealNormSpace st not X is trivial & X is Reflexive holds
( X is separable iff DualSp (DualSp X) is separable )