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

hereby :: thesis: ( a is P -ordered implies ( - (abs (P,a)) <= P,a & a <= P, abs (P,a) ) )

assume AS: ( - (abs (P,a)) <= P,a & a <= P, abs (P,a) ) ; :: thesis: a is P -ordered

now :: thesis: a is P -ordered

assume not a is P -ordered ; :: thesis: contradiction
then B: ( - (- (1. R)) <= P,a & a <= P, - (1. R) ) by AS, av00;
( 0. R < P, 1. R & - (1. R) < P, 0. R ) by c20;
then - (1. R) < P, 1. R by c2, c3;
then a < P, 1. R by B, c2, c3;
hence contradiction by B, c2; :: thesis: verum

end;

hence a is P -ordered ; :: thesis: verum

end;

X: P + P c= P by REALALG1:def 14;

now :: thesis: ( a in P \/ (- P) implies ( - (abs (P,a)) <= P,a & a <= P, abs (P,a) ) )

assume a in P \/ (- P) ; :: thesis: ( - (abs (P,a)) <= P,a & a <= P, abs (P,a) )

per cases then ( a in P or a in - P ) by XBOOLE_0:def 3;

suppose A: a in P ; :: thesis: ( - (abs (P,a)) <= P,a & a <= P, abs (P,a) )

then B: abs (P,a) = a by defa;
then a + (abs (P,a)) in P + P by A;
hence ( - (abs (P,a)) <= P,a & a <= P, abs (P,a) ) by X, B, c1; :: thesis: verum

end;

suppose a in - P ; :: thesis: ( - (abs (P,a)) <= P,a & a <= P, abs (P,a) )

then A1: ( abs (P,a) = - a & - a in - (- P) ) by defa;
then B: ( - (abs (P,a)) = - (- a) & - a in P ) ;
(abs (P,a)) + (- a) in P + P by A1;
hence ( - (abs (P,a)) <= P,a & a <= P, abs (P,a) ) by X, B, c1; :: thesis: verum

end;

end;

end;

hence ( a is P -ordered implies ( - (abs (P,a)) <= P,a & a <= P, abs (P,a) ) ) ; :: thesis: verum