for f, g, h being eventually-nonnegative Real_Sequence st f in Big_Omega g & g in Big_Omega h holds
f in Big_Omega h