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 )