let f be eventually-nonnegative Real_Sequence; :: thesis: f in Big_Theta f
( f in Big_Oh f & f in Big_Omega f ) by Th10, Th20;
hence f in Big_Theta f by XBOOLE_0:def 4; :: thesis: verum