let X be RealNormSpace; :: thesis: for x being Point of (DualSp X)
for M being non empty Subspace of X holds { ||.(x - m).|| where m is Point of (DualSp X) : m in Ort_Comp M } is non empty real-membered bounded_below set
let x be Point of (DualSp X); :: thesis: for M being non empty Subspace of X holds { ||.(x - m).|| where m is Point of (DualSp X) : m in Ort_Comp M } is non empty real-membered bounded_below set
let M be non empty Subspace of X; :: thesis: { ||.(x - m).|| where m is Point of (DualSp X) : m in Ort_Comp M } is non empty real-membered bounded_below set
set B = { ||.(x - m).|| where m is Point of (DualSp X) : m in Ort_Comp M } ;
0. (DualSp X) in Ort_Comp M by RLSUB_1:17;
then A1P: ||.(x - (0. (DualSp X))).|| in { ||.(x - m).|| where m is Point of (DualSp X) : m in Ort_Comp M } ;
{ ||.(x - m).|| where m is Point of (DualSp X) : m in Ort_Comp M } c= REAL

proof

let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in { ||.(x - m).|| where m is Point of (DualSp X) : m in Ort_Comp M } or r in REAL )
assume r in { ||.(x - m).|| where m is Point of (DualSp X) : m in Ort_Comp M } ; :: thesis: r in REAL
then ex m being Point of (DualSp X) st
( r = ||.(x - m).|| & m in Ort_Comp M ) ;
hence r in REAL ; :: thesis: verum

end;

then reconsider B = { ||.(x - m).|| where m is Point of (DualSp X) : m in Ort_Comp M } as real-membered set ;
B is bounded_below

proof

reconsider r0 = 0 as Real ;
take r0 ; :: according to XXREAL_2:def 9 :: thesis: r0 is LowerBound of B
let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in B or r0 <= r )
assume r in B ; :: thesis: r0 <= r
then ex m being Point of (DualSp X) st
( r = ||.(x - m).|| & m in Ort_Comp M ) ;
hence r0 <= r ; :: thesis: verum

end;

hence { ||.(x - m).|| where m is Point of (DualSp X) : m in Ort_Comp M } is non empty real-membered bounded_below set by A1P; :: thesis: verum