set M = LowPositives(Poly) P;
set K = Polynom-Ring R;
X2: 0. R in P by ord3;

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

let x, y be Element of (Polynom-Ring R); :: thesis: ( x in LowPositives(Poly) P & y in LowPositives(Poly) P implies b₁ + b₂ in LowPositives(Poly) P )
assume AS: ( x in LowPositives(Poly) P & y in LowPositives(Poly) P ) ; :: thesis: b₁ + b₂ in LowPositives(Poly) P
then consider p being Polynomial of R such that
H1: ( x = p & p . (min* { i where i is Nat : p . i <> 0. R } ) in P ) ;
consider q being Polynomial of R such that
H2: ( y = q & q . (min* { i where i is Nat : q . i <> 0. R } ) in P ) by AS;

per cases ( p is zero or q is zero or ( not p is zero & not q is zero ) ) ;

suppose A: p is zero ; :: thesis: b₁ + b₂ in LowPositives(Poly) P

B: min* { i where i is Nat : (p + q) . i <> 0. R } = min* { i where i is Nat : q . i <> 0. R } by lemlowp0, A;
(p + q) . (min* { i where i is Nat : q . i <> 0. R } ) = q . (min* { i where i is Nat : q . i <> 0. R } ) by A, POLYNOM3:28;
then p + q in { r where r is Polynomial of R : r . (min* { i where i is Nat : r . i <> 0. R } ) in P } by B, H2;
hence x + y in LowPositives(Poly) P by H1, H2, POLYNOM3:def 10; :: thesis: verum

end;

suppose A: q is zero ; :: thesis: b₁ + b₂ in LowPositives(Poly) P

then B: min* { i where i is Nat : (p + q) . i <> 0. R } = min* { i where i is Nat : p . i <> 0. R } by lemlowp0;
(p + q) . (min* { i where i is Nat : p . i <> 0. R } ) = p . (min* { i where i is Nat : p . i <> 0. R } ) by A, POLYNOM3:28;
then p + q in { r where r is Polynomial of R : r . (min* { i where i is Nat : r . i <> 0. R } ) in P } by B, H1;
hence x + y in LowPositives(Poly) P by H1, H2, POLYNOM3:def 10; :: thesis: verum

end;

suppose ( not p is zero & not q is zero ) ; :: thesis: b₁ + b₂ in LowPositives(Poly) P

then (p + q) . (min* { i where i is Nat : (p + q) . i <> 0. R } ) in P by H1, H2, lemlowp1;
then p + q in { r where r is Polynomial of R : r . (min* { i where i is Nat : r . i <> 0. R } ) in P } ;
hence x + y in LowPositives(Poly) P by H1, H2, POLYNOM3:def 10; :: thesis: verum

end;

end;

end;

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

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

let o be object ; :: thesis: ( o in {(0. (Polynom-Ring R))} implies o in (LowPositives(Poly) P) /\ (- (LowPositives(Poly) P)) )
assume X00: o in {(0. (Polynom-Ring R))} ; :: thesis: o in (LowPositives(Poly) P) /\ (- (LowPositives(Poly) P))
then X0: o = 0. (Polynom-Ring R) by TARSKI:def 1;
then X1: o = 0_. R by POLYNOM3:def 10;
reconsider q = o as Polynomial of R by X00, POLYNOM3:def 10;
q . (min* { i where i is Nat : q . i <> 0. R } ) = 0. R by X1, FUNCOP_1:7;
then X3: q in LowPositives(Poly) P by X2;
reconsider q = q as Element of (Polynom-Ring R) by POLYNOM3:def 10;
- q in { (- p) where p is Element of (Polynom-Ring R) : p in LowPositives(Poly) P } by X3;
hence o in (LowPositives(Poly) P) /\ (- (LowPositives(Poly) P)) by X0, X3, XBOOLE_0:def 4; :: thesis: verum

end;

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

let o be object ; :: thesis: ( o in (LowPositives(Poly) P) /\ (- (LowPositives(Poly) P)) implies o in {(0. (Polynom-Ring R))} )
assume o in (LowPositives(Poly) P) /\ (- (LowPositives(Poly) P)) ; :: thesis: o in {(0. (Polynom-Ring R))}
then X1: ( o in LowPositives(Poly) P & o in - (LowPositives(Poly) P) ) by XBOOLE_0:def 4;
then consider p being Polynomial of R such that
X2: ( o = p & p . (min* { i where i is Nat : p . i <> 0. R } ) in P ) ;
set V = { i where i is Nat : p . i <> 0. R } ;
consider x being Element of (Polynom-Ring R) such that
X3: ( o = - x & x in LowPositives(Poly) P ) by X1;
consider q being Polynomial of R such that
X4: ( x = q & q . (min* { i where i is Nat : q . i <> 0. R } ) in P ) by X3;

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

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

end;

now :: thesis: not { i where i is Nat : p . i <> 0. R } <> {}

assume { i where i is Nat : p . i <> 0. R } <> {} ; :: thesis: contradiction
then reconsider cp = { i where i is Nat : p . i <> 0. R } as non empty Subset of NAT by X8, TARSKI:def 3;
min* cp in cp by NAT_1:def 1;
then consider i being Nat such that
X9: ( i = min* cp & p . i <> 0. R ) ;
X15: - (- x) = x ;
then X13: q . i = (- p) . i by X4, X3, X2, lemminuspoly
.= - (p . i) by BHSP_1:44 ;

now :: thesis: not q . i = 0. R

assume q . i = 0. R ; :: thesis: contradiction
then - (- (p . i)) = - (0. R) by X13;
hence contradiction by X9; :: thesis: verum

end;

then X11: i in { i where i is Nat : q . i <> 0. R } ;

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

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

end;

then reconsider cq = { i where i is Nat : q . i <> 0. R } as non empty Subset of NAT by X11, TARSKI:def 3;

now :: thesis: for k being Nat st k in { i where i is Nat : q . i <> 0. R } holds
i <= k

let k be Nat; :: thesis: ( k in { i where i is Nat : q . i <> 0. R } implies i <= k )
assume k in { i where i is Nat : q . i <> 0. R } ; :: thesis: i <= k
then consider j being Nat such that
X14: ( k = j & q . j <> 0. R ) ;
q . j = (- p) . j by X15, X4, X3, X2, lemminuspoly
.= - (p . j) by BHSP_1:44 ;
then p . j <> 0. R by X14;
then j in cp ;
hence i <= k by X14, X9, NAT_1:def 1; :: thesis: verum

end;

then min* cq = i by X11, NAT_1:def 1;
then p . i = (- q) . (min* { i where i is Nat : q . i <> 0. R } ) by X4, X3, X2, lemminuspoly
.= - (q . (min* { i where i is Nat : q . i <> 0. R } )) by BHSP_1:44 ;
then p . (min* { i where i is Nat : p . i <> 0. R } ) in - P by X4, X9;
then p . (min* { i where i is Nat : p . i <> 0. R } ) in P /\ (- P) by X2, XBOOLE_0:def 4;
then p . (min* { i where i is Nat : p . i <> 0. R } ) in {(0. R)} by defppc;
hence contradiction by X9, TARSKI:def 1; :: thesis: verum

end;

then p = 0_. R by lemlp0
.= 0. (Polynom-Ring R) by POLYNOM3:def 10 ;
hence o in {(0. (Polynom-Ring R))} by X2, TARSKI:def 1; :: thesis: verum

end;

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