:: deftheorem Def9 defines BoundedLinearFunctionals DUALSP01:def 10 :
for X being RealNormSpace
for b₂ being Subset of (X *') holds
( b₂ = BoundedLinearFunctionals X iff for x being set holds
( x in b₂ iff x is Lipschitzian linear-Functional of X ) );