:: deftheorem defines Big_Theta ASYMPT_0:def 11 :
for f being eventually-nonnegative Real_Sequence holds Big_Theta f = (Big_Oh f) /\ (Big_Omega f);