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

hereby :: thesis: ( a is O -ordered implies 0. R <= O, abs (O,a) )

assume 0. R <= O, abs (O,a) ; :: thesis: a is O -ordered
then C: - (1. R) < O, abs (O,a) by avb5, c20;

per cases ( a in O or a in - O or ( not a in O & not a in - O ) ) ;

suppose a in O ; :: thesis: a is O -ordered

hence a is O -ordered by XBOOLE_0:def 3; :: thesis: verum

end;

suppose a in - O ; :: thesis: a is O -ordered

hence a is O -ordered by XBOOLE_0:def 3; :: thesis: verum

end;

suppose ( not a in O & not a in - O ) ; :: thesis: a is O -ordered

hence a is O -ordered by C, defa; :: thesis: verum

end;

end;

end;

assume a is O -ordered ; :: thesis: 0. R <= O, abs (O,a)

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

suppose a in O ; :: thesis: 0. R <= O, abs (O,a)

hence 0. R <= O, abs (O,a) by defa; :: thesis: verum

end;

suppose D: a in - O ; :: thesis: 0. R <= O, abs (O,a)

then - a in - (- O) ;
hence 0. R <= O, abs (O,a) by D, defa; :: thesis: verum

end;

end;