let f be Real_Sequence; :: thesis: ( f is positive implies f is eventually-positive )
assume A1: f is positive ; :: thesis: f is eventually-positive
take 0 ; :: according to ASYMPT_0:def 4 :: thesis: for n being Element of NAT st n >= 0 holds
f . n > 0
let n be Element of NAT ; :: thesis: ( n >= 0 implies f . n > 0 )
assume n >= 0 ; :: thesis: f . n > 0
thus f . n > 0 by A1, Def5; :: thesis: verum