reconsider f = chi ((REAL \ I),I) as Function of I,REAL by Th11;
take f ; :: thesis: f is HK-integrable
REAL \ I misses I by XBOOLE_1:79;
hence f is HK-integrable by Th29; :: thesis: verum