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

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