:: deftheorem Def2 defines eventually-nonnegative ASYMPT_0:def 2 :

for f being Real_Sequence holds

( f is eventually-nonnegative iff ex N being Nat st

for n being Nat st n >= N holds

f . n >= 0 );

for f being Real_Sequence holds

( f is eventually-nonnegative iff ex N being Nat st

for n being Nat st n >= N holds

f . n >= 0 );