theorem Th27: :: POLYRED:27

for n being Ordinal
for T being connected TermOrder of n
for L being non empty addLoopStr
for p, q, r being Polynomial of n,L st p <= q,T & q <= r,T holds
p <= r,T