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 ) )
assume A1: i1 in k -SD_Sub_S ; :: thesis: ( i1 >= - (Radix (k -' 1)) & i1 <= (Radix (k -' 1)) - 1 )
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;
then consider i being Element of INT such that
A2: i = i1 and
A3: ( - (Radix (k -' 1)) <= i & i <= (Radix (k -' 1)) - 1 ) by A1;
thus ( i1 >= - (Radix (k -' 1)) & i1 <= (Radix (k -' 1)) - 1 ) by A2, A3; :: thesis: verum