::
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
);