let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st f is_left_divergent_to+infty_in x0 holds
ex r being Real st
( 0 < r & f | ].(x0 - r),x0.[ is bounded_below )
let x0 be Real; :: thesis: ( f is_left_divergent_to+infty_in x0 implies ex r being Real st
( 0 < r & f | ].(x0 - r),x0.[ is bounded_below ) )
assume A1: f is_left_divergent_to+infty_in x0 ; :: thesis: ex r being Real st
( 0 < r & f | ].(x0 - r),x0.[ is bounded_below )
consider r being Real such that
A2: r < x0 and
A3: for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds
1 < f . r1 by A1, LIMFUNC2:8;
set R = x0 - r;
for r1 being object st r1 in dom (f | ].(x0 - (x0 - r)),x0.[) holds
1 < (f | ].(x0 - (x0 - r)),x0.[) . r1

proof

let r1 be object ; :: thesis: ( r1 in dom (f | ].(x0 - (x0 - r)),x0.[) implies 1 < (f | ].(x0 - (x0 - r)),x0.[) . r1 )
assume A4: r1 in dom (f | ].(x0 - (x0 - r)),x0.[) ; :: thesis: 1 < (f | ].(x0 - (x0 - r)),x0.[) . r1
then reconsider r1 = r1 as Real ;
r1 in (dom f) /\ ].(x0 - (x0 - r)),x0.[ by A4, RELAT_1:61;
then A5: ( r1 in dom f & r1 in ].(x0 - (x0 - r)),x0.[ ) by XBOOLE_0:def 4;
then ( x0 - (x0 - r) < r1 & r1 < x0 ) by XXREAL_1:4;
then 1 < f . r1 by A3, A5;
hence 1 < (f | ].(x0 - (x0 - r)),x0.[) . r1 by A5, FUNCT_1:49; :: thesis: verum

end;

then f | ].(x0 - (x0 - r)),x0.[ is bounded_below by SEQ_2:def 2;
hence ex r being Real st
( 0 < r & f | ].(x0 - r),x0.[ is bounded_below ) by A2, XREAL_1:50; :: thesis: verum