theorem :: ASYMPT_0:33

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