:: deftheorem Def2 defines sgn ABSVALUE:def 2 :
for x being Real holds
( ( 0 < x implies sgn x = 1 ) & ( x < 0 implies sgn x = - 1 ) & ( not 0 < x & not x < 0 implies sgn x = 0 ) );