for x being Integer
for k being Nat holds
( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 )