theorem :: ASYMPT_0:25

for f, t being positive Real_Sequence holds
( t in Big_Omega f iff ex d being Real st
( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) ) )