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 that
A1: f /" g is convergent and
A2: lim (f /" g) = 0 ; :: thesis: ( f in Big_Oh g & not f in Big_Theta g )

now

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, A2, Th16; :: thesis: verum

end;

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