:: deftheorem defines weakly-sequentially-compact DUALSP03:def 6 :
for X being RealNormSpace
for X0 being non empty Subset of X holds
( X0 is weakly-sequentially-compact iff for seq being sequence of X0 ex seq1 being sequence of X st
( seq1 is subsequence of seq & seq1 is weakly-convergent & w-lim seq1 in X ) );