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 -negative iff 0. R <= P,a )
let P be Preordering of R; :: thesis: for a being P -ordered Element of R holds
( not a is P -negative iff 0. R <= P,a )
let a be P -ordered Element of R; :: thesis: ( not a is P -negative iff 0. R <= P,a )
H: ( a in P \/ (- P) & P /\ (- P) = {(0. R)} ) by REALALG1:def 14, defppp;

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

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

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

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

hence 0. R <= P,a by H, XBOOLE_0:def 3; :: thesis: verum

end;

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

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

end;

end;

end;

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

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

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

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

end;

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

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 -negative by XBOOLE_0:def 5; :: thesis: verum

end;

end;