let X be RealBanachSpace; 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; ( 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 )
; ( 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
; 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 )
; contradiction
set S = { ||.x.|| where x is Point of X : x in X0 } ;
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]
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 )
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; verum