theorem Lm55: :: DUALSP03:14

for X being RealBanachSpace
for T being Subset of (DualSp X) st ( for x being Point of X ex K being Real st
( 0 <= K & ( for f being Point of (DualSp X) st f in T holds
|.(f . x).| <= K ) ) ) holds
ex L being Real st
( 0 <= L & ( for f being Point of (DualSp X) st f in T holds
||.f.|| <= L ) )