let f, g be eventually-positive Real_Sequence; :: thesis: ( f /" g is convergent & lim (f /" g) = 0 implies ( g in Big_Omega f & not f in Big_Omega g ) )
assume ( f /" g is convergent & lim (f /" g) = 0 ) ; :: thesis: ( g in Big_Omega f & not f in Big_Omega g )
then ( f in Big_Oh g & not g in Big_Oh f ) by Th16;
hence ( g in Big_Omega f & not f in Big_Omega g ) by Th19; :: thesis: verum