let R be preordered Ring; :: thesis: for P being Preordering of R
for a being b₁ -ordered Element of R holds
( not a is P -positive iff a <= P, 0. R )
let P be Preordering of R; :: thesis: for a being P -ordered Element of R holds
( not a is P -positive iff a <= P, 0. R )
let a be P -ordered Element of R; :: thesis: ( not a is P -positive iff a <= P, 0. R )
H: ( a in P \/ (- P) & P /\ (- P) = {(0. R)} ) by REALALG1:def 14, defppp;

hereby :: thesis: ( a <= P, 0. R implies not a is P -positive )

assume not a is P -positive ; :: thesis: a <= P, 0. R

per cases then ( not a in P or a in {(0. R)} ) by XBOOLE_0:def 5;

suppose not a in P ; :: thesis: a <= P, 0. R

then a in - P by H, XBOOLE_0:def 3;
then - a in - (- P) ;
hence a <= P, 0. R ; :: thesis: verum

end;

suppose a in {(0. R)} ; :: thesis: a <= P, 0. R

then a = 0. R by TARSKI:def 1;
hence a <= P, 0. R by c1; :: thesis: verum

end;

end;

end;

assume a <= P, 0. R ; :: thesis: not a is P -positive
then C: - (- a) in - P ;

per cases ( a = 0. R or a <> 0. R ) ;

suppose a = 0. R ; :: thesis: not a is P -positive

then a in {(0. R)} by TARSKI:def 1;
hence not a is P -positive by XBOOLE_0:def 5; :: thesis: verum

end;

suppose D: a <> 0. R ; :: thesis: not a is P -positive

now :: thesis: not a in P

assume a in P ; :: thesis: contradiction
then a in {(0. R)} by C, H;
hence contradiction by D, TARSKI:def 1; :: thesis: verum

end;

hence not a is P -positive by XBOOLE_0:def 5; :: thesis: verum

end;

end;