:: deftheorem defines -SD RADIX_1:def 2 :
for k being Nat holds k -SD = { e where e is Element of INT : ( e <= (Radix k) - 1 & e >= (- (Radix k)) + 1 ) } ;