:: deftheorem Def10 defines BoundedLinearFunctionals DUALSP04:def 8 :
for X being RealUnitarySpace
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 ) );