let R be preordered Ring; :: thesis: for P being Preordering of R
for a, b being Element of R holds abs (P,(a - b)) = abs (P,(b - a))
let O be Preordering of R; :: thesis: for a, b being Element of R holds abs (O,(a - b)) = abs (O,(b - a))
let a, b be Element of R; :: thesis: abs (O,(a - b)) = abs (O,(b - a))

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

suppose A: a - b in O ; :: thesis: abs (O,(a - b)) = abs (O,(b - a))

then - (a - b) in - O ;
then b - a in - O by RLVECT_1:33;
hence abs (O,(b - a)) = - (b - a) by defa
.= a - b by RLVECT_1:33
.= abs (O,(a - b)) by A, defa ;
:: thesis: verum

end;

suppose A: a - b in - O ; :: thesis: abs (O,(a - b)) = abs (O,(b - a))

then - (a - b) in - (- O) ;
then B: b - a in O by RLVECT_1:33;
thus abs (O,(a - b)) = - (a - b) by A, defa
.= b - a by RLVECT_1:33
.= abs (O,(b - a)) by B, defa ; :: thesis: verum

end;

suppose A: ( not a - b in O & not a - b in - O ) ; :: thesis: abs (O,(a - b)) = abs (O,(b - a))

then B: abs (O,(a - b)) = - (1. R) by defa;
( not b - a in O & not b - a in - O )

proof

assume ( b - a in O or b - a in - O ) ; :: thesis: contradiction
then ( - (b - a) in - O or - (b - a) in - (- O) ) ;
hence contradiction by A, RLVECT_1:33; :: thesis: verum

end;

hence abs (O,(a - b)) = abs (O,(b - a)) by B, defa; :: thesis: verum

end;

end;