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 O be Preordering of R; :: thesis: for a being Element of R holds
( ( - (abs (O,a)) <= O,a & a <= O, abs (O,a) ) iff a is O -ordered )
let a be Element of R; :: thesis: ( ( - (abs (O,a)) <= O,a & a <= O, abs (O,a) ) iff a is O -ordered )
hereby :: thesis: ( a is O -ordered implies ( - (abs (O,a)) <= O,a & a <= O, abs (O,a) ) )
assume AS: ( - (abs (O,a)) <= O,a & a <= O, abs (O,a) ) ; :: thesis: a is O -ordered
per cases ( a in - O or a in O or ( not a in O & not a in - O ) ) ;
suppose ( not a in O & not a in - O ) ; :: thesis: a is O -ordered
then ( 1. R <= O,a & a <= O, - (1. R) ) by AS, defa;
then F: 1. R <= O, - (1. R) by c3;
- (1. R) < O, 0. R by c20;
then - (1. R) < O, 1. R by c20, avb6;
hence a is O -ordered by F, c2; :: thesis: verum
end;
end;
end;
assume G: a is O -ordered ; :: thesis: ( - (abs (O,a)) <= O,a & a <= O, abs (O,a) )
Y: 0. R <= O, abs (O,a) by G, av0;
then X: ( abs (O,a) in O & O + O c= O ) by REALALG1:def 14;
per cases ( a in O or a in - O ) by G, XBOOLE_0:def 3;
suppose A: a in O ; :: thesis: ( - (abs (O,a)) <= O,a & a <= O, abs (O,a) )
then C: abs (O,a) = a by defa;
then B: (abs (O,a)) - a = 0. R by RLVECT_1:15;
a + (abs (O,a)) in O + O by C, A;
hence - (abs (O,a)) <= O,a by X; :: thesis: a <= O, abs (O,a)
thus a <= O, abs (O,a) by B, REALALG1:25; :: thesis: verum
end;
suppose A: a in - O ; :: thesis: ( - (abs (O,a)) <= O,a & a <= O, abs (O,a) )
then abs (O,a) = - a by defa;
then (abs (O,a)) - (- a) = 0. R by RLVECT_1:15;
then (abs (O,a)) + a in O by REALALG1:25;
hence - (abs (O,a)) <= O,a ; :: thesis: a <= O, abs (O,a)
- a in - (- O) by A;
then (abs (O,a)) + (- a) in O + O by Y;
hence a <= O, abs (O,a) by X; :: thesis: verum
end;
end;