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

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

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

now :: thesis: not abs (O,a) = - (1. R)

assume abs (O,a) = - (1. R) ; :: thesis: contradiction
then (- (1. R)) + (1. R) = (0. R) + (1. R) by B;
hence contradiction by RLVECT_1:5; :: thesis: verum

end;

then C: a is O -ordered by av00;

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

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

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

end;

suppose not a in O ; :: thesis: a = 0. R

then a in - O by C, XBOOLE_0:def 3;
then - a = 0. R by B, defa;
then - (- a) = 0. R ;
hence a = 0. R ; :: thesis: verum

end;

end;

end;

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