:: deftheorem defines <= POLYRED:def 2 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p, q being Polynomial of n,L holds
( p <= q,T iff [(Support p),(Support q)] in FinOrd RelStr(# (Bags n),T #) );