:: deftheorem defines integrable INTEGRA1:def 16 :
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL holds
( f is integrable iff ( f is upper_integrable & f is lower_integrable & upper_integral f = lower_integral f ) );