:: deftheorem defines separable NORMSP_3:def 3 :
for X being RealNormSpace holds
( X is separable iff LinearTopSpaceNorm X is separable );