let n be Ordinal; :: thesis: 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
let T be connected admissible TermOrder of n; :: thesis: 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
let L be non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p, q being Polynomial of n,L holds HT ((p - q),T) <= max ((HT (p,T)),(HT (q,T)),T),T
let p, q be Polynomial of n,L; :: thesis: HT ((p - q),T) <= max ((HT (p,T)),(HT (q,T)),T),T
HT ((p + (- q)),T) <= max ((HT (p,T)),(HT ((- q),T)),T),T by TERMORD:34;
then HT ((p - q),T) <= max ((HT (p,T)),(HT ((- q),T)),T),T by POLYNOM1:def 7;
hence HT ((p - q),T) <= max ((HT (p,T)),(HT (q,T)),T),T by Th6; :: thesis: verum