let R be non degenerated preordered Ring; :: thesis: for P being Preordering of R holds Positives(Poly) P <> LowPositives(Poly) P
let P be Preordering of R; :: thesis: Positives(Poly) P <> LowPositives(Poly) P
set p = rpoly (1,(1. R));
reconsider cp = { i where i is Nat : (rpoly (1,(1. R))) . i <> 0. R } as non empty Subset of NAT by lemlp1;
deg (rpoly (1,(1. R))) = 1 by HURWITZ:27;
then (len (rpoly (1,(1. R)))) -' 1 = 1 by XREAL_0:def 2;
then (rpoly (1,(1. R))) . ((len (rpoly (1,(1. R)))) -' 1) = 1_ R by HURWITZ:25;
then B: LC (rpoly (1,(1. R))) = 1. R ;
A: 1. R in P by ord3;
E: (rpoly (1,(1. R))) . 0 = - ((power R) . ((1. R),(0 + 1))) by HURWITZ:25
.= - (((power R) . ((1. R),0)) * (1. R)) by GROUP_1:def 7
.= - ((1_ R) * (1. R)) by GROUP_1:def 7
.= - (1. R) ;
now :: thesis: not - (1. R) = 0. R
assume - (1. R) = 0. R ; :: thesis: contradiction
then - (- (1. R)) = 0. R ;
hence contradiction ; :: thesis: verum
end;
then 0 in cp by E;
then C: min* cp = 0 by NAT_1:def 1;
now :: thesis: not rpoly (1,(1. R)) in LowPositives(Poly) P
assume rpoly (1,(1. R)) in LowPositives(Poly) P ; :: thesis: contradiction
then consider q being Polynomial of R such that
H: ( q = rpoly (1,(1. R)) & q . (min* { i where i is Nat : q . i <> 0. R } ) in P ) ;
thus contradiction by H, C, E, ord4; :: thesis: verum
end;
hence Positives(Poly) P <> LowPositives(Poly) P by A, B; :: thesis: verum