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