theorem :: DUALSP02:20

for X being RealNormSpace
for L being non empty Subset of X st not X is trivial & ( for f being Point of (DualSp X) ex Y1 being Subset of REAL st
( Y1 = { |.(f . x).| where x is Point of X : x in L } & sup Y1 < +infty ) ) holds
ex Y being Subset of REAL st
( Y = { ||.x.|| where x is Point of X : x in L } & sup Y < +infty )