theorem av3: :: REALALG2:70

for R being preordered domRing
for P being Preordering of R
for a being Element of R holds
( abs (P,a) = - a iff a <= P, 0. R )