let X be RealBanachSpace; :: thesis: for X0 being non empty Subset of X st not X is trivial & X is Reflexive & X0 is weakly-sequentially-compact holds
ex S being non empty Subset of REAL st
( S = { ||.x.|| where x is Point of X : x in X0 } & S is bounded_above )
let X0 be non empty Subset of X; :: thesis: ( not X is trivial & X is Reflexive & X0 is weakly-sequentially-compact implies ex S being non empty Subset of REAL st
( S = { ||.x.|| where x is Point of X : x in X0 } & S is bounded_above ) )
assume AS1: ( not X is trivial & X is Reflexive ) ; :: thesis: ( not X0 is weakly-sequentially-compact or ex S being non empty Subset of REAL st
( S = { ||.x.|| where x is Point of X : x in X0 } & S is bounded_above ) )
assume AS2: X0 is weakly-sequentially-compact ; :: thesis: ex S being non empty Subset of REAL st
( S = { ||.x.|| where x is Point of X : x in X0 } & S is bounded_above )
assume B1: for S being non empty Subset of REAL holds
( not S = { ||.x.|| where x is Point of X : x in X0 } or not S is bounded_above ) ; :: thesis: contradiction
set S = { ||.x.|| where x is Point of X : x in X0 } ;
now :: thesis: for r being object st r in { ||.x.|| where x is Point of X : x in X0 } holds
r in REAL
let r be object ; :: thesis: ( r in { ||.x.|| where x is Point of X : x in X0 } implies r in REAL )
assume r in { ||.x.|| where x is Point of X : x in X0 } ; :: thesis: r in REAL
then ex x being Point of X st
( r = ||.x.|| & x in X0 ) ;
hence r in REAL ; :: thesis: verum
end;
then A11: { ||.x.|| where x is Point of X : x in X0 } c= REAL ;
consider x0 being object such that
A12: x0 in X0 by XBOOLE_0:def 1;
reconsider x0 = x0 as Point of X by A12;
||.x0.|| in { ||.x.|| where x is Point of X : x in X0 } by A12;
then reconsider S = { ||.x.|| where x is Point of X : x in X0 } as non empty Subset of REAL by A11;
defpred S1[ Nat, Point of X] means ( $1 <= ||.$2.|| & $2 in X0 );
P1: for n being Element of NAT ex x being Point of X st S1[n,x]
proof
assume ex n being Element of NAT st
for x being Point of X holds not S1[n,x] ; :: thesis: contradiction
then consider n being Element of NAT such that
Q1: for x being Point of X holds not S1[n,x] ;
for r being ExtReal st r in S holds
r <= n
proof
let r be ExtReal; :: thesis: ( r in S implies r <= n )
assume r in S ; :: thesis: r <= n
then ex x being Point of X st
( r = ||.x.|| & x in X0 ) ;
hence r <= n by Q1; :: thesis: verum
end;
then n is UpperBound of S by XXREAL_2:def 1;
then S is bounded_above ;
hence contradiction by B1; :: thesis: verum
end;
consider seq0 being Function of NAT, the carrier of X such that
P2: for n being Element of NAT holds S1[n,seq0 . n] from FUNCT_2:sch 3(P1);
 P3: for n being Nat holds
( n <= ||.(seq0 . n).|| & seq0 . n in X0 )
proof
let n be Nat; :: thesis: ( n <= ||.(seq0 . n).|| & seq0 . n in X0 )
n is Element of NAT by ORDINAL1:def 12;
hence ( n <= ||.(seq0 . n).|| & seq0 . n in X0 ) by P2; :: thesis: verum
end;
for n being Element of NAT holds seq0 . n in X0 by P3;
then rng seq0 c= X0 by FUNCT_2:114;
then reconsider seq = seq0 as sequence of X0 by FUNCT_2:6;
consider seq1 being sequence of X such that
A3: ( seq1 is subsequence of seq & seq1 is weakly-convergent & w-lim seq1 in X ) by AS2;
||.seq1.|| is bounded by A3, AS1, Th79;
then consider r being Real such that
A4: for n being Nat holds ||.seq1.|| . n < r by SEQ_2:def 3;
set n = [/r\] + 1;
||.seq1.|| . 0 < r by A4;
then ||.(seq1 . 0).|| < r by NORMSP_0:def 4;
then 0 <= [/r\] + 1 by INT_1:32;
then [/r\] + 1 in NAT by INT_1:3;
then reconsider n = [/r\] + 1 as Nat ;
consider N being V132() sequence of NAT such that
A52: seq1 = seq * N by A3, VALUED_0:def 17;
set m = N . n;
seq0 . (N . n) = seq1 . n by A52, FUNCT_2:15, ORDINAL1:def 12;
then A54: N . n <= ||.(seq1 . n).|| by P3;
n <= N . n by SEQM_3:14;
then B55: n <= ||.(seq1 . n).|| by A54, XXREAL_0:2;
||.seq1.|| . n < r by A4;
then ||.(seq1 . n).|| < r by NORMSP_0:def 4;
hence contradiction by B55, XXREAL_0:2, INT_1:32; :: thesis: verum