let f, g be eventually-positive Real_Sequence; :: thesis: ( f /" g is divergent_to+infty implies ( f in Big_Omega g & not f in Big_Theta g ) )
assume f /" g is divergent_to+infty ; :: thesis: ( f in Big_Omega g & not f in Big_Theta g )
then ( not f in Big_Oh g & g in Big_Oh f ) by Th17;
hence ( f in Big_Omega g & not f in Big_Theta g ) by Th19, XBOOLE_0:def 4; :: thesis: verum