theorem :: LIMFUNC2:67

for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & ex r being Real st
( 0 < r & ( ( (dom f1) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f1) /\ ].(x0 - r),x0.[ holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f2) /\ ].(x0 - r),x0.[ holds
f1 . g <= f2 . g ) ) ) ) holds
lim_left (f1,x0) <= lim_left (f2,x0)