let V be RealNormSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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

hence 0 <= lower_bound (NormVSets (V,W,v)) by XXREAL_2:def 4; :: thesis: 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; :: thesis: verum

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; :: thesis: 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; :: thesis: ( 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

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 0 <= lower_bound (NormVSets (V,W,v)) by XXREAL_2:def 4; :: thesis: 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; :: thesis: verum