:: deftheorem defines HK-integrable COUSIN2:def 10 :
for I being non empty closed_interval Subset of REAL
for f being Function of I,REAL holds
( f is HK-integrable iff ex J being Real st
for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - J).| <= epsilon );