:: deftheorem DefX1 defines Big_Oh_poly ASYMPT_3:def 2 :
for b₁ being Subset of (RAlgebra NAT) holds
( b₁ = Big_Oh_poly iff for x being object holds
( x in b₁ iff x is polynomially-abs-bounded Function of NAT,REAL ) );