for f being eventually-nonnegative Real_Sequence holds f in Big_Omega f