let R be non degenerated preordered Ring; :: thesis: for P being Preordering of R
for p, q being non zero Polynomial of R st p . (min* { i where i is Nat : p . i <> 0. R } ) in P & q . (min* { i where i is Nat : q . i <> 0. R } ) in P holds
(p + q) . (min* { i where i is Nat : (p + q) . i <> 0. R } ) in P
let P be Preordering of R; :: thesis: for p, q being non zero Polynomial of R st p . (min* { i where i is Nat : p . i <> 0. R } ) in P & q . (min* { i where i is Nat : q . i <> 0. R } ) in P holds
(p + q) . (min* { i where i is Nat : (p + q) . i <> 0. R } ) in P
let p, q be non zero Polynomial of R; :: thesis: ( p . (min* { i where i is Nat : p . i <> 0. R } ) in P & q . (min* { i where i is Nat : q . i <> 0. R } ) in P implies (p + q) . (min* { i where i is Nat : (p + q) . i <> 0. R } ) in P )
assume AS: ( p . (min* { i where i is Nat : p . i <> 0. R } ) in P & q . (min* { i where i is Nat : q . i <> 0. R } ) in P ) ; :: thesis: (p + q) . (min* { i where i is Nat : (p + q) . i <> 0. R } ) in P
reconsider cp = { i where i is Nat : p . i <> 0. R } , cq = { i where i is Nat : q . i <> 0. R } as non empty Subset of NAT by lemlp1;
Z1: ( P + P c= P & P /\ (- P) = {(0. R)} ) by defppc;

now :: thesis: for o being object st o in { i where i is Nat : (p + q) . i <> 0. R } holds
o in NAT

let o be object ; :: thesis: ( o in { i where i is Nat : (p + q) . i <> 0. R } implies o in NAT )
assume o in { i where i is Nat : (p + q) . i <> 0. R } ; :: thesis: o in NAT
then consider i being Nat such that
H1: ( o = i & (p + q) . i <> 0. R ) ;
thus o in NAT by H1, ORDINAL1:def 12; :: thesis: verum

end;

then reconsider cpq = { i where i is Nat : (p + q) . i <> 0. R } as Subset of NAT by TARSKI:def 3;

per cases ( min* cp > min* cq or min* cp < min* cq or min* cp = min* cq ) by XXREAL_0:1;

suppose AS1: min* cp > min* cq ; :: thesis: (p + q) . (min* { i where i is Nat : (p + q) . i <> 0. R } ) in P

not min* cq in cp by AS1, NAT_1:def 1;
then p . (min* cq) = 0. R ;
then (p + q) . (min* cq) = (0. R) + (q . (min* cq)) by NORMSP_1:def 2;
hence (p + q) . (min* { i where i is Nat : (p + q) . i <> 0. R } ) in P by AS1, AS, lemlowp1a1; :: thesis: verum

end;

suppose AS1: min* cp < min* cq ; :: thesis: (p + q) . (min* { i where i is Nat : (p + q) . i <> 0. R } ) in P

not min* cp in cq by AS1, NAT_1:def 1;
then q . (min* cp) = 0. R ;
then (p + q) . (min* cp) = (0. R) + (p . (min* cp)) by NORMSP_1:def 2;
hence (p + q) . (min* { i where i is Nat : (p + q) . i <> 0. R } ) in P by AS1, AS, lemlowp1a1; :: thesis: verum

end;

suppose XX: min* cp = min* cq ; :: thesis: (p + q) . (min* { i where i is Nat : (p + q) . i <> 0. R } ) in P

then D1: (p + q) . (min* cp) = (p . (min* cp)) + (q . (min* cq)) by NORMSP_1:def 2;

now :: thesis: not 0. R = (p . (min* cp)) + (q . (min* cp))

assume 0. R = (p . (min* cp)) + (q . (min* cp)) ; :: thesis: contradiction
then p . (min* cp) = - (q . (min* cp)) by RLVECT_1:6;
then p . (min* cp) in - P by AS, XX;
then Y: p . (min* cp) in P /\ (- P) by AS, XBOOLE_0:def 4;
min* cp in cp by NAT_1:def 1;
then consider w1 being Nat such that
H2: ( w1 = min* cp & p . w1 <> 0. R ) ;
thus contradiction by Y, H2, Z1, TARSKI:def 1; :: thesis: verum

end;

then min* cpq = min ((min* cp),(min* cq)) by XX, lemlowp1b
.= min* cp by XX ;
hence (p + q) . (min* { i where i is Nat : (p + q) . i <> 0. R } ) in P by D1, AS, IDEAL_1:def 1; :: thesis: verum

end;

end;