theorem Th21: :: DUALSP06:21

for V being RealNormSpace
for x being Point of V
for M being non empty Subspace of V st not x in 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 V : m in M } & U = { (x .|. y) where y is Point of (DualSp V) : ( y in Ort_Comp M & ||.y.|| <= 1 ) } & inf L = sup U & sup U in U & ( 0 < inf L implies ex v being Point of (DualSp V) st
( ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L ) ) & ( for m0 being Point of V st m0 in M & ||.(x - m0).|| = inf L holds
for v being Point of (DualSp V) st ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L holds
x - m0,v are_parallel ) )