:: deftheorem defines absolute_value REALALG2:def 11 :
for R being ordered Ring
for O being Ordering of R
for a being Element of R holds
( ( a in O implies absolute_value (O,a) = a ) & ( not a in O implies absolute_value (O,a) = - a ) );