theorem Lm65a: :: DUALSP02:3

for V being RealNormSpace
for x0 being Point of V st x0 <> 0. V holds
ex G being Point of (DualSp V) st
( (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / ||.x0.|| )