theorem :: DUALSP06:22

for V being RealNormSpace
for x, m0 being Point of V
for M being non empty Subspace of V st not x in M & m0 in M holds
( ( for m being Point of V st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) iff ex p being Point of (DualSp V) st
( p in Ort_Comp M & p <> 0. (DualSp V) & x - m0,p are_parallel ) )