theorem Th24: :: DUALSP06:24

for X being RealNormSpace
for x being Point of (DualSp X)
for M being non empty Subspace of X holds { (y .|. x) where y is Point of X : ( y in M & ||.y.|| <= 1 ) } is non empty real-membered bounded_above set