for X being RealUnitarySpace
for S being Subset of X st S is summable_set holds
for e being Real st 0 < e holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= S holds
|.(((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))).| < e ) )