theorem Th15: :: ASYMPT_0:15

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