:: deftheorem defines < POLYRED:def 3 :
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 ( p <= q,T & Support p <> Support q ) );