:: deftheorem defines Bound2Lipschitz DUALSP04:def 9 :
for X being RealUnitarySpace
for f being object holds Bound2Lipschitz (f,X) = In (f,(BoundedLinearFunctionals X));