for V being RealNormSpace
for x being Point of V st not V is trivial holds
( ex X being non empty Subset of REAL st
( X = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| = 1 } & ||.x.|| = upper_bound X ) & ex Y being non empty Subset of REAL st
( Y = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| <= 1 } & ||.x.|| = upper_bound Y ) )