:: deftheorem Def1 defines |. ABSVALUE:def 1 :
for x being Real holds
( ( 0 <= x implies |.x.| = x ) & ( not 0 <= x implies |.x.| = - x ) );