theorem :: LIMFUNC3:43

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