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