theorem
:: ASYMPT_0:24
for
f
,
g
being
eventually-positive
Real_Sequence
st
f
/"
g
is
divergent_to+infty
holds
( not
g
in
Big_Omega
f
&
f
in
Big_Omega
g
)