theorem :: LIMFUNC2:30

for x0 being Real
for f being PartFunc of REAL,REAL st ex r being Real st
( 0 < r & f | ].x0,(x0 + r).[ is decreasing & not f | ].x0,(x0 + r).[ is bounded_above ) & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ) holds
f is_right_divergent_to+infty_in x0 by Th29;