reconsider f = chi (I,I) as PartFunc of I,REAL by Th11;
reconsider f = f as integrable Function of I,REAL by INTEGRA4:2;
f is bounded by Th14;
hence ex b₁ being integrable Function of I,REAL st b₁ is bounded ; :: thesis: verum