theorem Th63: :: DUALSP02:1

for V being RealNormSpace
for X being SubRealNormSpace of V
for x0 being Point of V
for d being Real st ex Z being non empty Subset of REAL st
( Z = { ||.(x - x0).|| where x is Point of V : x in X } & d = lower_bound Z & lower_bound Z > 0 ) holds
( not x0 in X & ex G being Point of (DualSp V) st
( ( for x being Point of V st x in X holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / d ) )