:: deftheorem Def7 defines norm-generated C0SP3:def 6 :
for X being non empty RLNormTopStruct holds
( X is norm-generated iff ex RNS being RealNormSpace st
( RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & the topology of X = the topology of (TopSpaceNorm RNS) ) );