theorem Th25: :: POLYRED:25

for n being Ordinal
for T being connected TermOrder of n
for L being non empty addLoopStr
for p being Polynomial of n,L holds p <= p,T by Lm11, ORDERS_1:3;