theorem :: DUALSP06:25

for V being RealNormSpace
for x being Point of (DualSp V)
for M being non empty Subspace of V
for SM being SubRealNormSpace of V st SM = RSubNormSpace M holds
ex L being non empty real-membered bounded_below set ex U being non empty real-membered bounded_above set st
( L = { ||.(x - m).|| where m is Point of (DualSp V) : m in Ort_Comp M } & U = { (y .|. x) where y is Point of V : ( y in M & ||.y.|| <= 1 ) } & ex m0 being Point of (DualSp V) ex fx being Lipschitzian linear-Functional of V ex xM being Point of (DualSp SM) st
( x = fx & xM = fx | the carrier of SM & m0 in Ort_Comp M & ||.(x - m0).|| = inf L & inf L in L & ||.(x - m0).|| = ||.xM.|| & ( for y being Point of V st ||.y.|| = 1 & y in M & fx . y = ||.(x - m0).|| holds
y,x - m0 are_parallel ) ) )