let R be preordered Ring; :: thesis: for P being Preordering of R
for a being b1 -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 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;