let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non empty 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 empty 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 23;
hence HT (p - q),T <= max (HT p,T),(HT q,T),T,T by Th6; :: thesis: verum