set P = Positives(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 (Positives(Poly) O) \/ (- (Positives(Poly) O))

let o be object ; :: thesis: ( o in the carrier of (Polynom-Ring R) implies b₁ in (Positives(Poly) O) \/ (- (Positives(Poly) O)) )
assume o in the carrier of (Polynom-Ring R) ; :: thesis: b₁ in (Positives(Poly) O) \/ (- (Positives(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 ( LC p in O or LC p in - O ) by X1, XBOOLE_0:def 3;

suppose LC p in O ; :: thesis: b₁ in (Positives(Poly) O) \/ (- (Positives(Poly) O))

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

end;

suppose LC p in - O ; :: thesis: b₁ in (Positives(Poly) O) \/ (- (Positives(Poly) O))

then consider a being Element of R such that
A: ( - a = LC p & a in O ) ;
reconsider b = - p as Element of (Polynom-Ring R) by POLYNOM3:def 10;
LC (- p) = (- p) . ((len p) -' 1) by POLYNOM4:8
.= - (p . ((len p) -' 1)) by BHSP_1:44
.= a by A ;
then - p in Positives(Poly) O by A;
then C: - b in - (Positives(Poly) O) ;
- b = - (- p) by lemminuspoly
.= p by HURWITZ:10 ;
hence o in (Positives(Poly) O) \/ (- (Positives(Poly) O)) by C, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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