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