set M = Positives(Poly) P;
set K = Polynom-Ring R;
X1: ( P + P c= P & P * P c= P ) by defppc;

now :: thesis: for x, y being Element of (Polynom-Ring R) st x in Positives(Poly) P & y in Positives(Poly) P holds
x + y in Positives(Poly) P

let x, y be Element of (Polynom-Ring R); :: thesis: ( x in Positives(Poly) P & y in Positives(Poly) P implies x + y in Positives(Poly) P )
assume AS: ( x in Positives(Poly) P & y in Positives(Poly) P ) ; :: thesis: x + y in Positives(Poly) P
then consider p being Polynomial of R such that
A: ( x = p & LC p in P ) ;
consider q being Polynomial of R such that
B: ( y = q & LC q in P ) by AS;
(LC p) + (LC q) in { (x + y) where x, y is Element of R : ( x in P & y in P ) } by A, B;
then C: (LC p) + (LC q) in P + P by IDEAL_1:def 19;

D: now :: thesis: ( (LC p) + (LC q) = 0. R implies ( LC p = 0. R & LC q = 0. R ) )

assume D1: (LC p) + (LC q) = 0. R ; :: thesis: ( LC p = 0. R & LC q = 0. R )
then LC q = - (LC p) by RLVECT_1:6;
then - (- (LC p)) in - P by B;
then LC p in P /\ (- P) by A, XBOOLE_0:def 4;
then LC p in {(0. R)} by defppc;
hence LC p = 0. R by TARSKI:def 1; :: thesis: LC q = 0. R
hence LC q = 0. R by D1; :: thesis: verum

end;

LC (p + q) in P

proof

per cases ( len p = len q or len p < len q or len p > len q ) by XXREAL_0:1;

suppose AS: len p = len q ; :: thesis: LC (p + q) in P

then C0: (p + q) . ((len p) -' 1) = (LC p) + (LC q) by NORMSP_1:def 2;
C11: ( len p is_at_least_length_of p & len p is_at_least_length_of q ) by AS, ALGSEQ_1:def 3;
C1: len (p + q) = len p

proof

now :: thesis: for m being Nat st m is_at_least_length_of p + q holds
len p <= m

let m be Nat; :: thesis: ( m is_at_least_length_of p + q implies len p <= m )
assume c13: m is_at_least_length_of p + q ; :: thesis: len p <= m
thus len p <= m :: thesis: verum

proof

assume C14: m < len p ; :: thesis: contradiction
then C15: (len p) - 1 = (len p) -' 1 by NAT_1:14, XREAL_1:233;
m < ((len p) - 1) + 1 by C14;
then p is zero by D, C0, c13, C15, NAT_1:13;
hence contradiction by C14, POLYNOM4:3; :: thesis: verum

end;

end;

hence len (p + q) = len p by C11, ALGSEQ_1:def 3, POLYNOM3:24; :: thesis: verum

end;

LC (p + q) = (LC p) + (LC q) by C1, AS, NORMSP_1:def 2;
hence LC (p + q) in P by C, X1; :: thesis: verum

end;

suppose AS: len p < len q ; :: thesis: LC (p + q) in P

then C11: len (p + q) = max ((len p),(len q)) by POLYNOM4:7
.= len q by AS, XXREAL_0:def 10 ;
C15: (len q) - 1 = (len q) -' 1 by AS, NAT_1:14, XREAL_1:233;
len p < ((len q) - 1) + 1 by AS;
then C13: len p <= (len q) -' 1 by C15, NAT_1:13;
len p is_at_least_length_of p by ALGSEQ_1:def 3;
then C12: p . ((len q) -' 1) = 0. R by C13;
LC (p + q) = (p . ((len q) -' 1)) + (q . ((len q) -' 1)) by NORMSP_1:def 2, C11
.= LC q by C12 ;
hence LC (p + q) in P by B; :: thesis: verum

end;

suppose AS: len p > len q ; :: thesis: LC (p + q) in P

then C11: len (p + q) = max ((len p),(len q)) by POLYNOM4:7
.= len p by AS, XXREAL_0:def 10 ;
C15: (len p) - 1 = (len p) -' 1 by XREAL_1:233, AS, NAT_1:14;
len q < ((len p) - 1) + 1 by AS;
then C13: len q <= (len p) -' 1 by C15, NAT_1:13;
len q is_at_least_length_of q by ALGSEQ_1:def 3;
then C12: q . ((len p) -' 1) = 0. R by C13;
LC (p + q) = (p . ((len p) -' 1)) + (q . ((len p) -' 1)) by NORMSP_1:def 2, C11
.= LC p by C12 ;
hence LC (p + q) in P by A; :: thesis: verum

end;

end;

end;

then p + q in { r where r is Polynomial of R : LC r in P } ;
hence x + y in Positives(Poly) P by A, B, POLYNOM3:def 10; :: thesis: verum

end;

hence Positives(Poly) P is add-closed ; :: thesis: Positives(Poly) P is negative-disjoint

X: now :: thesis: for o being object st o in {(0. (Polynom-Ring R))} holds
o in (Positives(Poly) P) /\ (- (Positives(Poly) P))

let o be object ; :: thesis: ( o in {(0. (Polynom-Ring R))} implies o in (Positives(Poly) P) /\ (- (Positives(Poly) P)) )
assume o in {(0. (Polynom-Ring R))} ; :: thesis: o in (Positives(Poly) P) /\ (- (Positives(Poly) P))
then o = 0. (Polynom-Ring R) by TARSKI:def 1;
then X1: o = 0_. R by POLYNOM3:def 10;
LC (0_. R) = 0. R by FUNCOP_1:7;
then LC (0_. R) in {(0. R)} by TARSKI:def 1;
then LC (0_. R) in P /\ (- P) by defppc;
then ( LC (0_. R) in P & LC (0_. R) in - P ) by XBOOLE_0:def 4;
then X3: 0_. R in Positives(Poly) P ;
reconsider q = 0_. R as Element of (Polynom-Ring R) by POLYNOM3:def 10;
X4: - q in { (- p) where p is Element of (Polynom-Ring R) : p in Positives(Poly) P } by X3;
len (- (0_. R)) = len (0_. R) by POLYNOM4:8
.= 0 by POLYNOM4:3 ;
then 0_. R = - (0_. R) by POLYNOM4:5
.= - q by lemminuspoly ;
hence o in (Positives(Poly) P) /\ (- (Positives(Poly) P)) by X1, X3, X4, XBOOLE_0:def 4; :: thesis: verum

end;

now :: thesis: for o being object st o in (Positives(Poly) P) /\ (- (Positives(Poly) P)) holds
o in {(0. (Polynom-Ring R))}

let o be object ; :: thesis: ( o in (Positives(Poly) P) /\ (- (Positives(Poly) P)) implies o in {(0. (Polynom-Ring R))} )
assume o in (Positives(Poly) P) /\ (- (Positives(Poly) P)) ; :: thesis: o in {(0. (Polynom-Ring R))}
then X1: ( o in Positives(Poly) P & o in - (Positives(Poly) P) ) by XBOOLE_0:def 4;
then consider p being Polynomial of R such that
X2: ( o = p & LC p in P ) ;
consider x being Element of (Polynom-Ring R) such that
X3: ( o = - x & x in Positives(Poly) P ) by X1;
consider q being Polynomial of R such that
X4: ( x = q & LC q in P ) by X3;
X6: p = - q by X4, X3, X2, lemminuspoly;
then len p = len q by POLYNOM4:8;
then LC p = - (LC q) by BHSP_1:44, X6;
then LC p in - P by X4;
then LC p in P /\ (- P) by X2, XBOOLE_0:def 4;
then LC p in {(0. R)} by defppc;
then p is zero by TARSKI:def 1;
then p = 0. (Polynom-Ring R) by POLYNOM3:def 10;
hence o in {(0. (Polynom-Ring R))} by X2, TARSKI:def 1; :: thesis: verum

end;

hence Positives(Poly) P is negative-disjoint by X, TARSKI:2; :: thesis: verum