let f, g be eventually-positive Real_Sequence; :: thesis: ( f /" g is divergent_to+infty implies ( not g in Big_Omega f & f in Big_Omega g ) )
assume f /" g is divergent_to+infty ; :: thesis: ( not g in Big_Omega f & f in Big_Omega g )
then ( g /" f is convergent & lim (g /" f) = 0 ) by Th5;
hence ( not g in Big_Omega f & f in Big_Omega g ) by Th23; :: thesis: verum