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