let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non empty right_zeroed addLoopStr
for p, q being Polynomial of n,L holds HT (p + q),T <= max (HT p,T),(HT q,T),T,T
let O be connected admissible TermOrder of n; :: thesis: for L being non empty right_zeroed addLoopStr
for p, q being Polynomial of n,L holds HT (p + q),O <= max (HT p,O),(HT q,O),O,O
let L be non empty right_zeroed addLoopStr ; :: thesis: for p, q being Polynomial of n,L holds HT (p + q),O <= max (HT p,O),(HT q,O),O,O
let p, q be Polynomial of n,L; :: thesis: HT (p + q),O <= max (HT p,O),(HT q,O),O,O

per cases ( HT (p + q),O in Support (p + q) or not HT (p + q),O in Support (p + q) ) ;

suppose A1: HT (p + q),O in Support (p + q) ; :: thesis: HT (p + q),O <= max (HT p,O),(HT q,O),O,O

A2: Support (p + q) c= (Support p) \/ (Support q) by POLYNOM1:79;

now

per cases ( HT (p + q),O in Support p or HT (p + q),O in Support q ) by A1, A2, XBOOLE_0:def 3;

case A3: HT (p + q),O in Support p ; :: thesis: HT (p + q),O <= max (HT p,O),(HT q,O),O,O

then A4: HT (p + q),O <= HT p,O,O by Def6;

now

per cases ( max (HT p,O),(HT q,O),O = HT p,O or max (HT p,O),(HT q,O),O = HT q,O ) by Th12;

case max (HT p,O),(HT q,O),O = HT p,O ; :: thesis: HT (p + q),O <= max (HT p,O),(HT q,O),O,O

hence HT (p + q),O <= max (HT p,O),(HT q,O),O,O by A3, Def6; :: thesis: verum

end;

case A5: max (HT p,O),(HT q,O),O = HT q,O ; :: thesis: HT (p + q),O <= max (HT p,O),(HT q,O),O,O

then HT p,O <= HT q,O,O by Th14;
hence HT (p + q),O <= max (HT p,O),(HT q,O),O,O by A4, A5, Th8; :: thesis: verum

end;

end;

end;

hence HT (p + q),O <= max (HT p,O),(HT q,O),O,O ; :: thesis: verum

end;

case A6: HT (p + q),O in Support q ; :: thesis: HT (p + q),O <= max (HT p,O),(HT q,O),O,O

then A7: HT (p + q),O <= HT q,O,O by Def6;

now

per cases ( max (HT p,O),(HT q,O),O = HT q,O or max (HT p,O),(HT q,O),O = HT p,O ) by Th12;

case max (HT p,O),(HT q,O),O = HT q,O ; :: thesis: HT (p + q),O <= max (HT p,O),(HT q,O),O,O

hence HT (p + q),O <= max (HT p,O),(HT q,O),O,O by A6, Def6; :: thesis: verum

end;

case A8: max (HT p,O),(HT q,O),O = HT p,O ; :: thesis: HT (p + q),O <= max (HT p,O),(HT q,O),O,O

then HT q,O <= HT p,O,O by Th14;
hence HT (p + q),O <= max (HT p,O),(HT q,O),O,O by A7, A8, Th8; :: thesis: verum

end;

end;

end;

hence HT (p + q),O <= max (HT p,O),(HT q,O),O,O ; :: thesis: verum

end;

end;

end;

hence HT (p + q),O <= max (HT p,O),(HT q,O),O,O ; :: thesis: verum

end;

suppose not HT (p + q),O in Support (p + q) ; :: thesis: HT (p + q),O <= max (HT p,O),(HT q,O),O,O

then ( Support (p + q) = {} & HT (p + q),O = EmptyBag n ) by Def6;
then [(HT (p + q),O),(max (HT p,O),(HT q,O),O)] in O by BAGORDER:def 7;
hence HT (p + q),O <= max (HT p,O),(HT q,O),O,O by Def2; :: thesis: verum

end;

end;