let X be RealNormSpace; :: thesis:
let L be non empty Subset of X; :: thesis:
assume that
A1: not X is trivial and
A2: for f being Point of (DualSp X) ex Y1 being Subset of REAL st
( Y1 = { |.(f . x).| where x is Point of X : x in L } & sup Y1 < +infty ) ; :: thesis:
A3: for f being Point of (DualSp X) ex Kf being Real st
( 0 <= Kf & ( for x being Point of X st x in L holds
|.(f . x).| <= Kf ) )

let f be Point of (DualSp X); :: thesis:
reconsider f1 = f as Lipschitzian linear-Functional of X by DUALSP01:def 10;
consider Y1 being Subset of REAL such that
B1: ( Y1 = { |.(f . x).| where x is Point of X : x in L } & sup Y1 < +infty ) by A2;
reconsider r0 = 0 as Real ;
for r being ExtReal st r in Y1 holds
r0 <= r

end;

then U5: r0 is LowerBound of Y1 by XXREAL_2:def 2;
then U3: r0 <= inf Y1 by XXREAL_2:def 4;
consider x0 being object such that
B11: x0 in L by XBOOLE_0:def 1;
reconsider x0 = x0 as Point of X by B11;
set y1 = |.(f . x0).|;
|.(f . x0).| in Y1 by B1, B11;
then U6: ( inf Y1 <= |.(f . x0).| & |.(f . x0).| <= sup Y1 ) by XXREAL_2:3, XXREAL_2:4;
then B2: sup Y1 in REAL by B1, U3, XXREAL_0:14;
reconsider Kf = sup Y1 as Real by B2;
BX: for x being Point of X st x in L holds
|.(f . x).| <= Kf

let x be Point of X; :: thesis:
assume C0: x in L ; :: thesis:
reconsider r = |.(f . x).| as Real ;
r in Y1 by C0, B1;
hence |.(f . x).| <= Kf by XXREAL_2:4; :: thesis:

end;

take Kf ; :: thesis:
thus ( 0 <= Kf & ( for x being Point of X st x in L holds
|.(f . x).| <= Kf ) ) by U5, U6, BX, XXREAL_2:def 4; :: thesis:

end;

consider M being Real such that
D1: ( 0 <= M & ( for x being Point of X st x in L holds
||.x.|| <= M ) ) by A1, A3, Th75;
set f = 0. (DualSp X);
consider x0 being object such that
B11: x0 in L by XBOOLE_0:def 1;
reconsider x0 = x0 as Point of X by B11;
set y1 = |.((0. (DualSp X)) . x0).|;
set Y = { ||.x.|| where x is Point of X : x in L } ;
D2: ||.x0.|| in { ||.x.|| where x is Point of X : x in L } by B11;
{ ||.x.|| where x is Point of X : x in L } c= REAL

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in { ||.x.|| where x is Point of X : x in L } ; :: thesis:
then ex x being Point of X st
( z = ||.x.|| & x in L ) ;
hence z in REAL ; :: thesis:

end;

then reconsider Y = { ||.x.|| where x is Point of X : x in L } as non empty Subset of REAL by D2;
for r being ExtReal st r in Y holds
r <= M

end;