theorem Th1: :: RADIX_3:1

for k being Nat
for i1 being Integer st i1 in k -SD_Sub holds
( (- (Radix (k -' 1))) - 1 <= i1 & i1 <= Radix (k -' 1) )