theorem
Th21
:
:: ASYMPT_0:21
for
f
,
g
,
h
being
eventually-nonnegative
Real_Sequence
st
f
in
Big_Omega
g
&
g
in
Big_Omega
h
holds
f
in
Big_Omega
h