theorem Th75: :: DUALSP02:19

for X being RealNormSpace
for L being Subset of X st not X is trivial & ( for f being Point of (DualSp X) ex Kf being Real st
( 0 <= Kf & ( for x being Point of X st x in L holds
|.(f . x).| <= Kf ) ) ) holds
ex M being Real st
( 0 <= M & ( for x being Point of X st x in L holds
||.x.|| <= M ) )