let X be RealNormSpace; :: thesis: ( not X is trivial & X is Reflexive implies ( X is separable iff DualSp (DualSp X) is separable ) )
assume A1: ( not X is trivial & X is Reflexive ) ; :: thesis: ( X is separable iff DualSp (DualSp X) is separable )
then consider DuX being SubRealNormSpace of DualSp (DualSp X), L being Lipschitzian LinearOperator of X,DuX such that
A2: ( L is bijective & DuX = Im (BidualFunc X) & ( for x being Point of X holds L . x = BiDual x ) & ( for x being Point of X holds ||.x.|| = ||.(L . x).|| ) ) by DUALSP02:10;
A3: Im (BidualFunc X) = DualSp (DualSp X) by A1, DUALSP02:22;
then reconsider L = L as Lipschitzian LinearOperator of X,(DualSp (DualSp X)) by A2;
L is isomorphism by A2, A3;
hence ( X is separable iff DualSp (DualSp X) is separable ) by Th31; :: thesis: verum