theorem Th20: :: ASYMPT_0:20

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