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

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

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

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

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

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

end;

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

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

end;

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

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

end;

end;

end;

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