theorem Th711: :: DUALSP03:15

for X being RealBanachSpace
for f being sequence of (DualSp X) st f is weakly*-convergent holds
( ||.f.|| is bounded & ||.(w*-lim f).|| <= lim_inf ||.f.|| )