for f being eventually-nonnegative Real_Sequence
for X being set holds Big_Theta (f,X) = (Big_Oh (f,X)) /\ (Big_Omega (f,X))