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 that
A1: f /" g is convergent and
A2: lim (f /" g) = 0 ; :: thesis: ( g in Big_Omega f & not f in Big_Omega g )
( f in Big_Oh g & not g in Big_Oh f ) by A1, A2, Th16;
hence ( g in Big_Omega f & not f in Big_Omega g ) by Th19; :: thesis: verum