theorem LM18: :: ASYMPT_3:16
0. R_Algebra_of_Big_Oh_poly = 0. (RAlgebra NAT) by defAlgebra;