:: deftheorem Def10 defines SD_Add_Carry RADIX_1:def 10 :
for x being Integer holds
( ( x > 2 implies SD_Add_Carry x = 1 ) & ( x < - 2 implies SD_Add_Carry x = - 1 ) & ( not x > 2 & not x < - 2 implies SD_Add_Carry x = 0 ) );