theorem Th9: :: RADIX_3:9

for k being Nat holds k -SD_Sub c= INT