let R be non degenerated preordered Ring; :: thesis: for P being Preordering of R
for a being Element of R holds
( not a is P -ordered iff abs (P,a) = - (1. R) )
let P be Preordering of R; :: thesis: for a being Element of R holds
( not a is P -ordered iff abs (P,a) = - (1. R) )
let a be Element of R; :: thesis: ( not a is P -ordered iff abs (P,a) = - (1. R) )

hereby :: thesis: ( abs (P,a) = - (1. R) implies not a is P -ordered )

assume not a is P -ordered ; :: thesis: abs (P,a) = - (1. R)
then ( not a in P & not a in - P ) by XBOOLE_0:def 3;
hence abs (P,a) = - (1. R) by defa; :: thesis: verum

end;

assume AS: abs (P,a) = - (1. R) ; :: thesis: not a is P -ordered
assume a is P -ordered ; :: thesis: contradiction
then 0. R <= P, abs (P,a) by av0;
hence contradiction by AS, REALALG1:26; :: thesis: verum