let X be RealNormSpace; :: thesis: for x being Point of (DualSp X)
for M being non empty Subspace of X holds { (y .|. x) where y is Point of X : ( y in M & ||.y.|| <= 1 ) } is non empty real-membered bounded_above set
let x be Point of (DualSp X); :: thesis: for M being non empty Subspace of X holds { (y .|. x) where y is Point of X : ( y in M & ||.y.|| <= 1 ) } is non empty real-membered bounded_above set
let M be non empty Subspace of X; :: thesis: { (y .|. x) where y is Point of X : ( y in M & ||.y.|| <= 1 ) } is non empty real-membered bounded_above set
set B = { (y .|. x) where y is Point of X : ( y in M & ||.y.|| <= 1 ) } ;
set z = 0. X;
A1: 0. X in M by RLSUB_1:17;
||.(0. X).|| = 0 ;
then A2P: (0. X) .|. x in { (y .|. x) where y is Point of X : ( y in M & ||.y.|| <= 1 ) } by A1;
{ (y .|. x) where y is Point of X : ( y in M & ||.y.|| <= 1 ) } c= REAL

proof

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

end;

then reconsider B = { (y .|. x) where y is Point of X : ( y in M & ||.y.|| <= 1 ) } as real-membered set ;
B is bounded_above

proof

reconsider r0 = ||.x.|| as Real ;
take r0 ; :: according to XXREAL_2:def 10 :: thesis: r0 is UpperBound of B
let r be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not r in B or r <= r0 )
assume r in B ; :: thesis: r <= r0
then consider y being Point of X such that
A3: ( r = y .|. x & y in M & ||.y.|| <= 1 ) ;
reconsider x0 = x as Lipschitzian linear-Functional of X by DUALSP01:def 10;
A4: |.(x0 . y).| <= ||.x.|| * ||.y.|| by DUALSP01:26;
||.x.|| * ||.y.|| <= ||.x.|| * 1 by A3, XREAL_1:64;
then A5: |.(x0 . y).| <= ||.x.|| by A4, XXREAL_0:2;
x0 . y <= |.(x0 . y).| by ABSVALUE:4;
hence r <= r0 by A5, XXREAL_0:2, A3; :: thesis: verum

end;

hence { (y .|. x) where y is Point of X : ( y in M & ||.y.|| <= 1 ) } is non empty real-membered bounded_above set by A2P; :: thesis: verum