:: deftheorem defines majorizes ASYMPT_0:def 8 :
for f, g being Real_Sequence holds
( g majorizes f iff ex N being Element of NAT st
for n being Element of NAT st n >= N holds
f . n <= g . n );