let V be RealNormSpace; :: thesis: for x being Point of V st not V is trivial holds
( ex X being non empty Subset of REAL st
( X = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| = 1 } & ||.x.|| = upper_bound X ) & ex Y being non empty Subset of REAL st
( Y = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| <= 1 } & ||.x.|| = upper_bound Y ) )
let x be Point of V; :: thesis: ( not V is trivial implies ( ex X being non empty Subset of REAL st
( X = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| = 1 } & ||.x.|| = upper_bound X ) & ex Y being non empty Subset of REAL st
( Y = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| <= 1 } & ||.x.|| = upper_bound Y ) ) )
assume AS: not V is trivial ; :: thesis: ( ex X being non empty Subset of REAL st
( X = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| = 1 } & ||.x.|| = upper_bound X ) & ex Y being non empty Subset of REAL st
( Y = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| <= 1 } & ||.x.|| = upper_bound Y ) )
set X = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| = 1 } ;
set Y = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| <= 1 } ;
consider F0 being Point of (DualSp V) such that
P1: ||.F0.|| = 1 by AS, Lm65A;
P2: ( |.((Bound2Lipschitz (F0,V)) . x).| in { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| = 1 } & |.((Bound2Lipschitz (F0,V)) . x).| in { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| <= 1 } ) by P1;
P3: { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| = 1 } c= { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| <= 1 }

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| = 1 } or z in { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| <= 1 } )
assume z in { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| = 1 } ; :: thesis: z in { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| <= 1 }
then ex F being Point of (DualSp V) st
( z = |.((Bound2Lipschitz (F,V)) . x).| & ||.F.|| = 1 ) ;
hence z in { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| <= 1 } ; :: thesis: verum

end;

P4: { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| <= 1 } c= REAL

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| <= 1 } or z in REAL )
assume z in { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| <= 1 } ; :: thesis: z in REAL
then ex F being Point of (DualSp V) st
( z = |.((Bound2Lipschitz (F,V)) . x).| & ||.F.|| <= 1 ) ;
hence z in REAL by XREAL_0:def 1; :: thesis: verum

end;

then reconsider Y = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| <= 1 } as non empty Subset of REAL by P2;
{ |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| = 1 } c= REAL by P3, P4;
then reconsider X = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| = 1 } as non empty Subset of REAL by P2;

per cases ( x = 0. V or x <> 0. V ) ;

suppose X1: x = 0. V ; :: thesis: ( ex X being non empty Subset of REAL st
( X = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| = 1 } & ||.x.|| = upper_bound X ) & ex Y being non empty Subset of REAL st
( Y = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| <= 1 } & ||.x.|| = upper_bound Y ) )

for t being object st t in Y holds
t in {0}

proof

let t be object ; :: thesis: ( t in Y implies t in {0} )
assume t in Y ; :: thesis: t in {0}
then ex F being Point of (DualSp V) st
( t = |.((Bound2Lipschitz (F,V)) . x).| & ||.F.|| <= 1 ) ;
then t = 0 by ABSVALUE:2, X1, HAHNBAN:20;
hence t in {0} by TARSKI:def 1; :: thesis: verum

end;

then P6: ( Y c= {0} & X c= {0} ) by P3;
ex z being object st z in X by XBOOLE_0:def 1;
then 0 in X by P6, TARSKI:def 1;
then ( X = {0} & Y = {0} ) by P6, P3, ZFMISC_1:31;
then ( upper_bound X = 0 & upper_bound Y = 0 ) by SEQ_4:9;
then ( ||.x.|| = upper_bound X & ||.x.|| = upper_bound Y ) by X1;
hence ( ex X being non empty Subset of REAL st
( X = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| = 1 } & ||.x.|| = upper_bound X ) & ex Y being non empty Subset of REAL st
( Y = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| <= 1 } & ||.x.|| = upper_bound Y ) ) ; :: thesis: verum

end;

suppose Z1: x <> 0. V ; :: thesis: ( ex X being non empty Subset of REAL st
( X = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| = 1 } & ||.x.|| = upper_bound X ) & ex Y being non empty Subset of REAL st
( Y = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| <= 1 } & ||.x.|| = upper_bound Y ) )

X6: for r being ExtReal st r in Y holds
r <= ||.x.||

proof

let r be ExtReal; :: thesis: ( r in Y implies r <= ||.x.|| )
assume r in Y ; :: thesis: r <= ||.x.||
then consider F being Point of (DualSp V) such that
X4: ( r = |.((Bound2Lipschitz (F,V)) . x).| & ||.F.|| <= 1 ) ;
X5: |.((Bound2Lipschitz (F,V)) . x).| <= ||.F.|| * ||.x.|| by DUALSP01:26, SUBSET_1:def 8;
||.F.|| * ||.x.|| <= 1 * ||.x.|| by X4, XREAL_1:64;
hence r <= ||.x.|| by X4, X5, XXREAL_0:2; :: thesis: verum

end;

then ||.x.|| is UpperBound of Y by XXREAL_2:def 1;
then X7: Y is bounded_above ;
then X8: upper_bound X <= upper_bound Y by P3, SEQ_4:48;
for r being Real st r in Y holds
r <= ||.x.|| by X6;
then X9: upper_bound Y <= ||.x.|| by SEQ_4:45;
then X10: upper_bound X <= ||.x.|| by X8, XXREAL_0:2;
consider F0 being Point of (DualSp V) such that
Y1: ( ||.F0.|| = 1 & (Bound2Lipschitz (F0,V)) . x = ||.x.|| ) by Lm65, Z1;
|.((Bound2Lipschitz (F0,V)) . x).| = ||.x.|| by Y1, ABSVALUE:def 1;
then Y3: ||.x.|| in X by Y1;
X is bounded_above by P3, X7, XXREAL_2:43;
then ||.x.|| <= upper_bound X by Y3, SEQ_4:def 1;
then ||.x.|| = upper_bound X by X10, XXREAL_0:1;
hence ( ex X being non empty Subset of REAL st
( X = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| = 1 } & ||.x.|| = upper_bound X ) & ex Y being non empty Subset of REAL st
( Y = { |.((Bound2Lipschitz (F,V)) . x).| where F is Point of (DualSp V) : ||.F.|| <= 1 } & ||.x.|| = upper_bound Y ) ) by X9, X8, XXREAL_0:1; :: thesis: verum

end;

end;