:: deftheorem defines is_summable_set_by BHSP_6:def 6 :
for X being RealUnitarySpace
for Y being Subset of X
for L being Functional of X holds
( Y is_summable_set_by L iff ex r being Real st
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) );