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

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