for x being set
for f being eventually-nonnegative Real_Sequence st x in Big_Omega f holds
x is eventually-nonnegative Real_Sequence