:: deftheorem defines -SD_Sub_S RADIX_3:def 1 :
for k being Nat holds k -SD_Sub_S = { e where e is Element of INT : ( e >= - (Radix (k -' 1)) & e <= (Radix (k -' 1)) - 1 ) } ;