for X being RealBanachSpace
for X0 being Subset of X
for vseq being sequence of (DualSp X) st ||.vseq.|| is bounded & X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) holds
vseq is weakly*-convergent