for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of n,L holds
( p < q,T iff ( ( p = 0_ (n,L) & q <> 0_ (n,L) ) or HT (p,T) < HT (q,T),T or ( HT (p,T) = HT (q,T) & Red (p,T) < Red (q,T),T ) ) ) by Lm15;