theorem
Th1
:
:: ASYMPT_0:1
for
f
being
Real_Sequence
for
N
being
Nat
st ( for
n
being
Nat
st
n
>=
N
holds
f
.
n
<=
f
.
(
n
+
1
)
) holds
for
n
,
m
being
Nat
st
N
<=
n
&
n
<=
m
holds
f
.
n
<=
f
.
m