for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of n,L holds HT ((p - q),T) <= max ((HT (p,T)),(HT (q,T)),T),T