for f being PartFunc of REAL,REAL
for b being Real st ex Intf being PartFunc of REAL,REAL st
( dom Intf = right_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,b,x) ) & ( Intf is divergent_in+infty_to+infty or Intf is divergent_in+infty_to-infty ) ) holds
not f is_+infty_ext_Riemann_integrable_on b