let x0 be Real; :: thesis: for f1, f being PartFunc of REAL ,REAL st f1 is_left_divergent_to-infty_in x0 & ex r being Real st
( 0 < r & ].(x0 - r),x0.[ c= (dom f) /\ (dom f1) & ( for g being Real st g in ].(x0 - r),x0.[ holds
f . g <= f1 . g ) ) holds
f is_left_divergent_to-infty_in x0
let f1, f be PartFunc of REAL ,REAL ; :: thesis: ( f1 is_left_divergent_to-infty_in x0 & ex r being Real st
( 0 < r & ].(x0 - r),x0.[ c= (dom f) /\ (dom f1) & ( for g being Real st g in ].(x0 - r),x0.[ holds
f . g <= f1 . g ) ) implies f is_left_divergent_to-infty_in x0 )
assume A1: f1 is_left_divergent_to-infty_in x0 ; :: thesis: ( for r being Real holds
( not 0 < r or not ].(x0 - r),x0.[ c= (dom f) /\ (dom f1) or ex g being Real st
( g in ].(x0 - r),x0.[ & not f . g <= f1 . g ) ) or f is_left_divergent_to-infty_in x0 )
given r being Real such that A2: ( 0 < r & ].(x0 - r),x0.[ c= (dom f) /\ (dom f1) & ( for g being Real st g in ].(x0 - r),x0.[ holds
f . g <= f1 . g ) ) ; :: thesis: f is_left_divergent_to-infty_in x0
( (dom f) /\ (dom f1) c= dom f & (dom f) /\ (dom f1) c= dom f1 ) by XBOOLE_1:17;
then A3: ( ].(x0 - r),x0.[ c= dom f & ].(x0 - r),x0.[ c= dom f1 ) by A2, XBOOLE_1:1;
then A4: ( ].(x0 - r),x0.[ = (dom f) /\ ].(x0 - r),x0.[ & ].(x0 - r),x0.[ = (dom f1) /\ ].(x0 - r),x0.[ ) by XBOOLE_1:28;
for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) by A2, A3, Th3;
hence f is_left_divergent_to-infty_in x0 by A1, A2, A4, Th40; :: thesis: verum