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

proof

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

end;

then reconsider B = { (x .|. y) where y is Point of (DualSp X) : ( y in Ort_Comp 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 (DualSp X) such that
A3: ( r = x .|. y & y in Ort_Comp M & ||.y.|| <= 1 ) ;
reconsider y0 = y as Lipschitzian linear-Functional of X by DUALSP01:def 10;
A4: |.(y0 . x).| <= ||.y.|| * ||.x.|| by DUALSP01:26;
||.y.|| * ||.x.|| <= 1 * ||.x.|| by A3, XREAL_1:64;
then A5: |.(y0 . x).| <= ||.x.|| by A4, XXREAL_0:2;
y0 . x <= |.(y0 . x).| by ABSVALUE:4;
hence r <= r0 by A5, XXREAL_0:2, A3; :: thesis: verum

end;

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