theorem :: ASYMPT_0:22

for f, g being eventually-positive Real_Sequence st f /" g is convergent & lim (f /" g) > 0 holds
Big_Omega f = Big_Omega g