:: deftheorem DEFCC defines HK-integral COUSIN2:def 11 :
for I being non empty closed_interval Subset of REAL
for f being Function of I,REAL st f is HK-integrable holds
for b₃ being Real holds
( b₃ = HK-integral f iff 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)) - b₃).| <= epsilon );