for X being RealBanachSpace
for X0 being non empty Subset of X st not X is trivial & X is Reflexive holds
( X0 is weakly-sequentially-compact iff ex S being non empty Subset of REAL st
( S = { ||.x.|| where x is Point of X : x in X0 } & S is bounded_above ) )