for X being RealUnitarySpace
for Y being Subset of X st Y is summable_set holds
Y is weakly_summable_set