theorem Lm73: :: DUALSP03:1

for X being strict RealNormSpace
for A being non empty Subset of X st ( for f being Point of (DualSp X) st ( for x being Point of X st x in A holds
(Bound2Lipschitz (f,X)) . x = 0 ) holds
Bound2Lipschitz (f,X) = 0. (DualSp X) ) holds
ClNLin A = X