theorem :: REALALG2:74

for R being preordered Ring
for P being Preordering of R
for a, b being Element of R holds abs (P,(a - b)) = abs (P,(b - a))