:: deftheorem Def3 defines positive ASYMPT_0:def 3 :
for f being Real_Sequence holds
( f is positive iff for n being Nat holds f . n > 0 );