theorem Lm64: :: DUALSP02:2

for V being RealNormSpace
for Y being non empty Subset of V
for x0 being Point of V st Y is linearly-closed & Y is closed & not x0 in Y holds
ex G being Point of (DualSp V) st
( ( for x being Point of V st x in Y holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 )