let R be preordered Ring; :: thesis: for P being Preordering of R
for a being Element of R holds abs (P,a) = abs (P,(- a))
let O be Preordering of R; :: thesis: for a being Element of R holds abs (O,a) = abs (O,(- a))
let a be Element of R; :: thesis: abs (O,a) = abs (O,(- a))
per cases ( a in - O or a in O or ( not a in O & not a in - O ) ) ;
suppose D: a in - O ; :: thesis: abs (O,a) = abs (O,(- a))
then E: abs (O,a) = - a by defa;
- a in - (- O) by D;
hence abs (O,a) = abs (O,(- a)) by E, defa; :: thesis: verum
end;
suppose D: a in O ; :: thesis: abs (O,a) = abs (O,(- a))
then E: abs (O,a) = a by defa;
( - a in - O & - (- a) = a ) by D;
hence abs (O,a) = abs (O,(- a)) by E, defa; :: thesis: verum
end;
suppose D: ( not a in O & not a in - O ) ; :: thesis: abs (O,a) = abs (O,(- a))
then E: abs (O,a) = - (1. R) by defa;
( not - a in O & not - a in - O )
proof
assume ( - a in O or - a in - O ) ; :: thesis: contradiction
then ( - (- a) in - O or - (- a) in - (- O) ) ;
hence contradiction by D; :: thesis: verum
end;
hence abs (O,a) = abs (O,(- a)) by E, defa; :: thesis: verum
end;
end;