let R be preordered domRing; :: thesis: for P being Preordering of R
for a being Element of R holds
( abs (P,a) = a iff 0. R <= P,a )
let O be Preordering of R; :: thesis: for a being Element of R holds
( abs (O,a) = a iff 0. R <= O,a )
let a be Element of R; :: thesis: ( abs (O,a) = a iff 0. R <= O,a )

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

assume B: abs (O,a) = a ; :: thesis: 0. R <= O,a

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

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

hence 0. R <= O,a ; :: thesis: verum

end;

suppose a in - O ; :: thesis: 0. R <= O,a

then a = - a by B, defa;
then a = 0. R by tA;
hence 0. R <= O,a by c1; :: thesis: verum

end;

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

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

end;

end;

end;

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