theorem LMQ23: :: NORMSP_3:66

for V being RealNormSpace
for W being Subspace of V
for v being VECTOR of V holds
( 0 <= lower_bound (NormVSets (V,W,v)) & lower_bound (NormVSets (V,W,v)) <= ||.v.|| )