theorem Th12: :: RADIX_3:12

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