let x0 be Real; :: thesis: for f, f1 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 f, f1 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 and
A3: ].(x0 - r),x0.[ c= (dom f) /\ (dom f1) and
A4: for g being Real st g in ].(x0 - r),x0.[ holds
f . g <= f1 . g ; :: thesis: f is_left_divergent_to-infty_in x0
A5: (dom f) /\ (dom f1) c= dom f by XBOOLE_1:17;
then A6: ].(x0 - r),x0.[ = (dom f) /\ ].(x0 - r),x0.[ by A3, XBOOLE_1:1, XBOOLE_1:28;
(dom f) /\ (dom f1) c= dom f1 by XBOOLE_1:17;
then A7: ].(x0 - r),x0.[ = (dom f1) /\ ].(x0 - r),x0.[ by A3, XBOOLE_1:1, 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, A5, Th3, XBOOLE_1:1;
hence f is_left_divergent_to-infty_in x0 by A1, A2, A4, A6, A7, Th34; :: thesis: verum