:: deftheorem defines Bound2Lipschitz DUALSP01:def 12 :
for X being RealNormSpace
for f being object holds Bound2Lipschitz (f,X) = In (f,(BoundedLinearFunctionals X));