let f, g be eventually-positive Real_Sequence; :: thesis: ( f /" g is convergent & lim (f /" g) = 0 implies ( f in Big_Oh g & not f in Big_Theta g ) )
assume A1: ( f /" g is convergent & lim (f /" g) = 0 ) ; :: thesis: ( f in Big_Oh g & not f in Big_Theta g )

now :: thesis: not f in Big_Theta g

assume f in Big_Theta g ; :: thesis: contradiction
then f in Big_Omega g by XBOOLE_0:def 4;
then g in Big_Oh f by Th19;
hence contradiction by A1, Th16; :: thesis: verum

end;

hence ( f in Big_Oh g & not f in Big_Theta g ) by A1, Th16; :: thesis: verum