set P = LowPositives(Poly) O;
set K = Polynom-Ring R;

X: now :: thesis: for o being object st o in the carrier of (Polynom-Ring R) holds
o in (LowPositives(Poly) O) \/ (- (LowPositives(Poly) O))

let o be object ; :: thesis: ( o in the carrier of (Polynom-Ring R) implies b₁ in (LowPositives(Poly) O) \/ (- (LowPositives(Poly) O)) )
assume o in the carrier of (Polynom-Ring R) ; :: thesis: b₁ in (LowPositives(Poly) O) \/ (- (LowPositives(Poly) O))
then reconsider p = o as Polynomial of R by POLYNOM3:def 10;
X1: O \/ (- O) = the carrier of R by defpc;

per cases ( p . (min* { i where i is Nat : p . i <> 0. R } ) in O or p . (min* { i where i is Nat : p . i <> 0. R } ) in - O ) by X1, XBOOLE_0:def 3;

suppose p . (min* { i where i is Nat : p . i <> 0. R } ) in O ; :: thesis: b₁ in (LowPositives(Poly) O) \/ (- (LowPositives(Poly) O))

then p in LowPositives(Poly) O ;
hence o in (LowPositives(Poly) O) \/ (- (LowPositives(Poly) O)) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose p . (min* { i where i is Nat : p . i <> 0. R } ) in - O ; :: thesis: b₁ in (LowPositives(Poly) O) \/ (- (LowPositives(Poly) O))

then consider a being Element of R such that
A: ( - a = p . (min* { i where i is Nat : p . i <> 0. R } ) & a in O ) ;
reconsider b = - p as Element of (Polynom-Ring R) by POLYNOM3:def 10;
(- p) . (min* { i where i is Nat : (- p) . i <> 0. R } ) = - (p . (min* { i where i is Nat : (- p) . i <> 0. R } )) by BHSP_1:44
.= - (p . (min* { i where i is Nat : p . i <> 0. R } )) by lemlowp2
.= a by A ;
then - p in LowPositives(Poly) O by A;
then C: - b in - (LowPositives(Poly) O) ;
- b = - (- p) by lemminuspoly
.= p by HURWITZ:10 ;
hence o in (LowPositives(Poly) O) \/ (- (LowPositives(Poly) O)) by C, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

for o being object st o in (LowPositives(Poly) O) \/ (- (LowPositives(Poly) O)) holds
o in the carrier of (Polynom-Ring R) ;
hence LowPositives(Poly) O is spanning by X, TARSKI:2; :: thesis: verum