let X be RealBanachSpace; :: thesis: for Y being Subset of X st X is Reflexive holds

ClNLin Y is Reflexive

let Y be Subset of X; :: thesis: ( X is Reflexive implies ClNLin Y is Reflexive )

assume A1: X is Reflexive ; :: thesis: ClNLin Y is Reflexive

ex Z being Subset of X st

( Z = the carrier of (Lin Y) & ClNLin Y = NLin (Cl Z) & Cl Z is linearly-closed & Cl Z <> {} ) by Th35;

hence ClNLin Y is Reflexive by A1, DUALSP02:24; :: thesis: verum

ClNLin Y is Reflexive

let Y be Subset of X; :: thesis: ( X is Reflexive implies ClNLin Y is Reflexive )

assume A1: X is Reflexive ; :: thesis: ClNLin Y is Reflexive

ex Z being Subset of X st

( Z = the carrier of (Lin Y) & ClNLin Y = NLin (Cl Z) & Cl Z is linearly-closed & Cl Z <> {} ) by Th35;

hence ClNLin Y is Reflexive by A1, DUALSP02:24; :: thesis: verum