:: deftheorem defines Lipschitzian BHSP_6:def 4 :
for X being RealUnitarySpace
for L being linear-Functional of X holds
( L is Lipschitzian iff ex K being Real st
( K > 0 & ( for x being Point of X holds |.(L . x).| <= K * ||.x.|| ) ) );