theorem Th31: :: NORMSP_4:24

for X, Y being RealNormSpace st ex L being Lipschitzian LinearOperator of X,Y st L is isomorphism holds
( X is separable iff Y is separable )