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

proof

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

end;

then reconsider B = { ||.(x - m).|| where m is Point of X : m in 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 X st
( r = ||.(x - m).|| & m in M ) ;
hence r0 <= r ; :: thesis: verum

end;

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