for F being preordered Field
for P being Preordering of F
for a being non zero b₂ -ordered Element of F holds abs (P,(a ")) = (abs (P,a)) "