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