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