:: deftheorem defa defines absolute_value REALALG2:def 10 :
for R being preordered Ring
for P being Preordering of R
for a being Element of R holds
( ( a in P implies absolute_value (P,a) = a ) & ( a in - P implies absolute_value (P,a) = - a ) & ( not a in P & not a in - P implies absolute_value (P,a) = - (1. R) ) );