theorem Th26: :: POLYRED:26

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 & q <= p,T ) iff Support p = Support q )