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

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

end;

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:

end;