theorem Th79: :: DUALSP03:10

for X being RealNormSpace
for x being sequence of X st not X is trivial & x is weakly-convergent holds
( ||.x.|| is bounded & ||.(w-lim x).|| <= lim_inf ||.x.|| & w-lim x in ClNLin (rng x) )