let k be Nat; :: thesis: for i1 being Integer st i1 in k -SD_Sub_S holds
( i1 >= - (Radix (k -' 1)) & i1 <= (Radix (k -' 1)) - 1 )
let i1 be Integer; :: thesis: ( i1 in k -SD_Sub_S implies ( i1 >= - (Radix (k -' 1)) & i1 <= (Radix (k -' 1)) - 1 ) )
A1: k -SD_Sub_S = { e where e is Element of INT : ( - (Radix (k -' 1)) <= e & e <= (Radix (k -' 1)) - 1 ) } by RADIX_3:def 1;
assume i1 in k -SD_Sub_S ; :: thesis: ( i1 >= - (Radix (k -' 1)) & i1 <= (Radix (k -' 1)) - 1 )
then ex i being Element of INT st
( i = i1 & - (Radix (k -' 1)) <= i & i <= (Radix (k -' 1)) - 1 ) by A1;
hence ( i1 >= - (Radix (k -' 1)) & i1 <= (Radix (k -' 1)) - 1 ) ; :: thesis: verum