let V be 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.|| )
let W be Subspace of V; for v being VECTOR of V holds
( 0 <= lower_bound (NormVSets (V,W,v)) & lower_bound (NormVSets (V,W,v)) <= ||.v.|| )
let v be VECTOR of V; ( 0 <= lower_bound (NormVSets (V,W,v)) & lower_bound (NormVSets (V,W,v)) <= ||.v.|| )
for r being ExtReal st r in NormVSets (V,W,v) holds
0 <= r
then
0 is LowerBound of NormVSets (V,W,v)
by XXREAL_2:def 2;
hence
0 <= lower_bound (NormVSets (V,W,v))
by XXREAL_2:def 4; lower_bound (NormVSets (V,W,v)) <= ||.v.||
v in v + W
by RLSUB_1:43;
then A2:
||.v.|| in NormVSets (V,W,v)
;
inf (NormVSets (V,W,v)) is LowerBound of NormVSets (V,W,v)
by XXREAL_2:def 4;
hence
lower_bound (NormVSets (V,W,v)) <= ||.v.||
by A2, XXREAL_2:def 2; verum