theorem Th1: :: BHSP_7:1

for X being RealUnitarySpace
for Y being Subset of X
for L being Functional of X holds
( Y is_summable_set_by L iff for e being Real st 0 < e holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) )