:: deftheorem Def4 defines eventually-positive ASYMPT_0:def 4 :
for f being Real_Sequence holds
( f is eventually-positive iff ex N being Nat st
for n being Nat st n >= N holds
f . n > 0 );