theorem :: DUALSP02:23

for X being RealNormSpace st not X is trivial & X is Reflexive holds
X is RealBanachSpace