theorem :: ASYMPT_0:18

for x being set

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

x is eventually-nonnegative Real_Sequence

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

x is eventually-nonnegative Real_Sequence