let V be RealNormSpace; :: thesis: for W being Subspace of V

for v being VECTOR of V holds NormVSets (V,W,v) is bounded_below

let W be Subspace of V; :: thesis: for v being VECTOR of V holds NormVSets (V,W,v) is bounded_below

let v be VECTOR of V; :: thesis: NormVSets (V,W,v) is bounded_below

for r being ExtReal st r in NormVSets (V,W,v) holds

0 <= r

hence NormVSets (V,W,v) is bounded_below by XXREAL_2:def 9; :: thesis: verum

for v being VECTOR of V holds NormVSets (V,W,v) is bounded_below

let W be Subspace of V; :: thesis: for v being VECTOR of V holds NormVSets (V,W,v) is bounded_below

let v be VECTOR of V; :: thesis: NormVSets (V,W,v) is bounded_below

for r being ExtReal st r in NormVSets (V,W,v) holds

0 <= r

proof

then
0 is LowerBound of NormVSets (V,W,v)
by XXREAL_2:def 2;
let r be ExtReal; :: thesis: ( r in NormVSets (V,W,v) implies 0 <= r )

assume r in NormVSets (V,W,v) ; :: thesis: 0 <= r

then consider x being VECTOR of V such that

A1: ( r = ||.x.|| & x in v + W ) ;

thus 0 <= r by A1; :: thesis: verum

end;assume r in NormVSets (V,W,v) ; :: thesis: 0 <= r

then consider x being VECTOR of V such that

A1: ( r = ||.x.|| & x in v + W ) ;

thus 0 <= r by A1; :: thesis: verum

hence NormVSets (V,W,v) is bounded_below by XXREAL_2:def 9; :: thesis: verum