for n being Ordinal
for T being connected TermOrder of n
for L being non empty addLoopStr
for p, q being Polynomial of n,L holds
( p <= q,T or q <= p,T )